Lemma doublecarry ( a : fpscommring hz ): carry ( carry a ) = carry a. 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.
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.