proposition: Lemma doublecarry ( a : fpscommring hz ): carry ( carry a ) = carry a.
proof: Proof. intros. assert ( forall n : nat, carry ( carry a ) n = carry a n ) as f. { intros. induction n. - unfold carry. simpl. apply hzremaindermoditerated. - unfold carry. simpl. change (precarry (fun n0 : nat => hzremaindermod m is (precarry a n0)) n) with ( precarry ( carry a ) n ). rewrite precarryandcarry. rewrite <- hzqrandcarryq. rewrite hzplusr0. rewrite hzremaindermoditerated. apply idpath. } apply ( funextfun _ _ f ). Defined.
imports: UniMath.PAdics.lemmas UniMath.PAdics.fps UniMath.PAdics.frac UniMath.PAdics.z_mod_p UniMath.NumberSystems.Integers