proposition: Lemma precarryandone : precarry p ( isaprimetoneq0 is ) 1 = @ringunel2 ( fpscommring hz ).
proof: Proof. intros. assert ( forall n : nat, precarry p ( isaprimetoneq0 is ) 1 n = @ringunel2 (fpscommring hz ) n ) as f. { intros n. induction n. - unfold precarry. apply idpath. - simpl. rewrite IHn. destruct n. + change ( @ringunel2 ( fpscommring hz ) 0%nat ) with 1%hz. rewrite hzqrand1q. rewrite hzplusr0. apply idpath. + change ( @ringunel2 ( fpscommring hz ) ( S n ) ) with 0%hz. rewrite hzqrand0q. rewrite hzplusr0. apply idpath. } apply ( funextfun _ _ f ). Defined.
imports: UniMath.PAdics.lemmas UniMath.PAdics.fps UniMath.PAdics.frac UniMath.PAdics.z_mod_p UniMath.NumberSystems.Integers