Lemma padiconecomputation : padicone = setquotpr ( carryequiv p ( isaprimetoneq0 is ) ) ( @ringunel2 ( fpscommring hz ) ). Proof. intros. apply idpath. Defined.
Require Import UniMath.PAdics.lemmas. Require Import UniMath.PAdics.fps. Require Import UniMath.PAdics.frac. Require Import UniMath.PAdics.z_mod_p. Require Import UniMath.NumberSystems.Integers.