proposition: Lemma precarryandtimesl ( a b : fpscommring hz ) ( n : nat ) : hzquotientmod m is ( precarry ( a * b ) n ) = ( quotientprecarry a * b ) n + hzquotientmod m is ( precarry ( carry a * b ) n ).
proof: Proof. intros. induction n. - unfold precarry. change ( ( a * b ) 0%nat ) with ( a 0%nat * b 0%nat ). change ( ( quotientprecarry a * b ) 0%nat ) with ( hzquotientmod m is ( a 0%nat ) * b 0%nat ). rewrite quotientandtimesrearrangel. change ( ( carry a * b ) 0%nat ) with ( hzremaindermod m is ( a 0%nat ) * b 0%nat ). apply idpath. - change ( precarry ( a * b ) ( S n ) ) with ( ( a * b ) ( S n ) + hzquotientmod m is ( precarry ( a * b ) n ) ). rewrite IHn. rewrite <- ( ringassoc1 hz ). assert ( ( ( a * b ) ( S n ) + ( quotientprecarry a * b ) n ) = ( @op2 ( fpscommring hz ) ( precarry a ) b ) ( S n ) ) as f. { change ( ( a * b ) ( S n ) ) with ( natsummation0 ( S n ) ( fun x : nat => a x * b ( sub ( S n ) x ) ) ). change ( ( quotientprecarry a * b ) n ) with ( natsummation0 n ( fun x : nat => quotientprecarry a x * b ( sub n x ) ) ). rewrite natsummationplusshift. change ( ( @op2 ( fpscommring hz ) ( precarry a ) b ) ( S n ) ) with ( natsummation0 ( S n ) ( fun x : nat => ( precarry a ) x * b ( sub ( S n ) x ) ) ). rewrite natsummationshift0. unfold precarry at 2. simpl. rewrite <- ( ringcomm1 hz ( a 0%nat * b ( S n ) ) _ ). apply ( maponpaths ( fun x : hz => a 0%nat * b ( S n ) + x ) ). apply natsummationpathsupperfixed. intros k j. unfold quotientprecarry. rewrite ( ringrdistr hz ). apply idpath. } rewrite f. rewrite hzquotientmodandplus. change ( @op2 ( fpscommring hz ) ( precarry a ) b ) with ( fpstimes hz ( precarry a ) b ). rewrite ( hzquotientandfpstimesl m is ( precarry a ) b ). change ( @op2 ( fpscommring hz ) ( carry a ) b ) with ( fpstimes hz ( carry a ) b ) at 1. unfold fpstimes at 1. unfold carry at 1. change (fun n0 : nat => let t' := fun m0 : nat => b (n0 - m0)%nat in natsummation0 n0 (fun x : nat => (hzremaindermod m is (precarry a x) * t' x)%ring)) with ( carry a * b ). change ( ( quotientprecarry a * b ) ( S n ) ) with ( natsummation0 ( S n ) ( fun i : nat => hzquotientmod m is ( precarry a i ) * b ( S n - i )%nat ) ). rewrite 2! hzplusassoc. apply ( maponpaths ( fun v => natsummation0 ( S n ) ( fun i : nat => hzquotientmod m is ( precarry a i ) * b ( S n - i )%nat ) + v ) ). change ( precarry ( carry a * b ) ( S n ) ) with ( ( carry a * b ) ( S n ) + hzquotientmod m is ( precarry ( carry a * b ) n ) ). change ((carry a * b) (S n) + hzquotientmod m is (precarry (carry a * b) n)) with ((carry a * b)%ring (S n) + hzquotientmod m is (precarry (carry a * b) n)%ring)%hz. rewrite ( hzquotientmodandplus m is ( ( carry a * b ) ( S n ) ) ( hzquotientmod m is ( precarry ( carry a * b ) n ) ) ). change ( ( carry a * b ) ( S n ) ) with ( natsummation0 ( S n ) ( fun i : nat => hzremaindermod m is ( precarry a i ) * b ( S n - i )%nat ) ). rewrite hzplusassoc. apply ( maponpaths ( fun v => ( hzquotientmod m is ( natsummation0 ( S n ) ( fun i : nat => hzremaindermod m is ( precarry a i ) * b ( S n - i )%nat ) ) ) + v ) ). apply ( maponpaths ( fun v => hzquotientmod m is ( hzquotientmod m is ( precarry ( carry a * b )%ring n ) ) + v ) ). apply maponpaths. apply ( maponpaths ( fun v => v + hzremaindermod m is ( hzquotientmod m is ( precarry ( carry a * b )%ring n ) ) ) ). unfold fpstimes. rewrite hzqrandnatsummation0r. rewrite ( hzqrandnatsummation0r m is ( fun i : nat => hzremaindermod m is ( precarry a i ) * b ( S n - i )%nat ) ). apply maponpaths. apply natsummationpathsupperfixed. intros j p. change ( hzremaindermod m is (hzremaindermod m is (precarry a j) * b ( sub ( S n ) j)) ) with ( hzremaindermod m is (hzremaindermod m is (precarry a j) * b (S n - j)%nat)%hz ). rewrite ( hzremaindermodandtimes m is ( hzremaindermod m is ( precarry a j ) ) ( b ( sub ( S n ) j ) ) ). rewrite hzremaindermoditerated. rewrite <- hzremaindermodandtimes. apply idpath. Defined.
imports: UniMath.PAdics.lemmas UniMath.PAdics.fps UniMath.PAdics.frac UniMath.PAdics.z_mod_p UniMath.NumberSystems.Integers