Lemma precarryandzero : precarry p ( isaprimetoneq0 is ) 0 = @ringunel1 ( fpscommring hz ). Proof. intros. assert ( forall n : nat, precarry p ( isaprimetoneq0 is ) 0 n = @ringunel1 (fpscommring hz ) n ) as f. { intros n. induction n. - unfold precarry. change ( @ringunel1 ( fpscommring hz ) 0%nat ) with 0%hz. apply idpath. - change ( ( ( @ringunel1 ( fpscommring hz ) ( S n ) + hzquotientmod p ( isaprimetoneq0 is ) ( precarry p ( isaprimetoneq0 is ) ( @ringunel1 ( fpscommring hz ) ) n ) ) ) = 0%hz ). rewrite IHn. change ( @ringunel1 ( fpscommring hz ) n ) with 0%hz. change ( @ringunel1 ( fpscommring hz ) ( S n ) ) with 0%hz. rewrite hzqrand0q. rewrite hzplusl0. apply idpath. } apply ( funextfun _ _ f ). 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.