Lemma carryandtimesl ( a b : fpscommring hz ) : carry ( a * b ) = carry ( carry a * b ). Proof. intros. assert ( forall n : nat, carry ( a * b ) n = carry ( carry a * b ) n ) as f. { intros n. destruct n. - unfold carry at 1 2. change ( precarry ( a * b ) 0%nat ) with ( a 0%nat * b 0%nat ). change ( precarry ( carry a * b ) 0%nat ) with ( carry a 0%nat * b 0%nat ). unfold carry. change (hzremaindermod m is (precarry a 0) * b 0%nat) with (hzremaindermod m is (precarry a 0) * b 0%nat )%hz. rewrite ( hzremaindermodandtimes m is ( hzremaindermod m is ( precarry a 0%nat ) ) ( b 0%nat ) ). rewrite hzremaindermoditerated. rewrite <- hzremaindermodandtimes. change ( precarry a 0%nat ) with ( a 0%nat ). apply idpath. - unfold carry at 1 2. change ( precarry ( a * b ) ( S n ) ) with ( ( a * b ) ( S n ) + hzquotientmod m is ( precarry ( a * b ) n ) ). rewrite precarryandtimesl. rewrite <- ( ringassoc1 hz ). rewrite hzremaindermodandplus. assert ( hzremaindermod m is ( ( a * b ) ( S n ) + ( quotientprecarry a * b ) n ) = hzremaindermod m is ( ( carry a * b ) ( S n ) ) ) as g. { change ( hzremaindermod m is ( ( natsummation0 ( S n ) ( fun u : nat => a u * b ( sub ( S n ) u ) ) ) + ( natsummation0 n ( fun u : nat => ( quotientprecarry a ) u * b ( sub n u ) ) ) ) = hzremaindermod m is ( natsummation0 ( S n ) ( fun u : nat => ( carry a ) u * b ( sub ( S n ) u ) ) ) ). rewrite ( natsummationplusshift n ). rewrite ( natsummationshift0 n ( fun u : nat => carry a u * b ( sub ( S n ) u ) ) ). assert ( hzremaindermod m is ( natsummation0 n ( fun x : nat => a ( S x ) * b ( sub ( S n ) ( S x ) ) + quotientprecarry a x * b ( sub n x ) ) ) = hzremaindermod m is (natsummation0 n ( fun x : nat => carry a ( S x ) * b ( sub ( S n ) ( S x ) ) ) ) ) as h. { rewrite hzqrandnatsummation0r. rewrite ( hzqrandnatsummation0r m is ( fun x : nat => carry a ( S x ) * b ( sub ( S n ) ( S x ) ) ) ). apply maponpaths. apply natsummationpathsupperfixed. intros j p. unfold quotientprecarry. simpl. intermediate_path (hzremaindermod m is ((a (S j) * b ( sub n j) + hzquotientmod m is (precarry a j) * b ( sub n j) )%hz)). + exact (idpath _). + rewrite <- ( hzrdistr ( a ( S j ) ) ( hzquotientmod m is ( precarry a j ) ) ( b ( sub n j ) ) ). rewrite hzremaindermodandtimes. change ( hzremaindermod m is (hzremaindermod m is (a (S j) + hzquotientmod m is (precarry a j)) * hzremaindermod m is (b ( sub n j))) = hzremaindermod m is (carry a (S j) * b(sub n j)) )%ring. rewrite <- ( hzremaindermoditerated m is (a (S j) + hzquotientmod m is (precarry a j)) ). unfold carry. rewrite <- hzremaindermodandtimes. apply idpath. } rewrite hzremaindermodandplus. rewrite h. rewrite <- hzremaindermodandplus. unfold carry at 3. rewrite ( hzremaindermodandplus m is _ ( hzremaindermod m is ( precarry a 0%nat ) * b ( sub ( S n ) 0%nat ) ) ). rewrite hzremaindermodandtimes. rewrite hzremaindermoditerated. rewrite <- hzremaindermodandtimes. change ( precarry a 0%nat ) with ( a 0%nat ). rewrite <- hzremaindermodandplus. rewrite hzpluscomm. apply idpath. } rewrite g. rewrite <- hzremaindermodandplus. 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.