proposition: Lemma padiczerocomputation : padiczero = setquotpr ( carryequiv p ( isaprimetoneq0 is ) ) ( @ringunel1 ( fpscommring hz ) ).
proof: Proof. intros. apply idpath. Defined.
imports: UniMath.PAdics.lemmas UniMath.PAdics.fps UniMath.PAdics.frac UniMath.PAdics.z_mod_p UniMath.NumberSystems.Integers