Lemma hzquotientandfpstimesl ( m : hz ) ( x : hzneq 0 m ) ( a b : nat -> hz ) ( upper : nat ) : hzquotientmod m x ( fpstimes hz a b upper ) = natsummation0 upper ( fun i : nat => hzquotientmod m x ( a i ) * b ( sub upper i ) ) + hzquotientmod m x ( natsummation0 upper ( fun i : nat => hzremaindermod m x ( a i ) * b ( sub upper i ) ) ). Proof. intros. destruct upper as [ | upper]. - simpl. unfold fpstimes. simpl. rewrite hzquotientandtimesl. rewrite hzplusassoc. apply ( maponpaths ( fun v : _ => hzquotientmod m x ( a 0%nat ) * b 0%nat + v ) ). rewrite ( hzquotientmodandtimes m x ( hzremaindermod m x ( a 0%nat ) ) ( b 0%nat ) ). rewrite <- hzqrandremainderq. rewrite hzmultx0. rewrite 2! hzmult0x. rewrite hzplusl0. rewrite hzremaindermoditerated. apply idpath. - unfold fpstimes. rewrite hzqrandnatsummation0q. assert ( forall n : nat, hzquotientmod m x (a n * b ( sub ( S upper ) n)%nat) = ( hzquotientmod m x ( a n ) * b ( sub ( S upper ) n ) + hzremaindermod m x ( a n ) * hzquotientmod m x ( b ( sub ( S upper ) n ) ) + hzquotientmod m x ( hzremaindermod m x ( a n ) * hzremaindermod m x ( b ( sub ( S upper ) n ) ) ) ) ) as f. { intro k. rewrite hzquotientandtimesl. apply idpath. } rewrite ( natsummationpathsupperfixed _ _ ( fun x0 p => f x0 ) ). rewrite ( natsummationplusdistr ( S upper ) ( fun x0 : nat => hzquotientmod m x (a x0) * b ( sub ( S upper ) x0)%nat + hzremaindermod m x (a x0) * hzquotientmod m x (b (S upper - x0)%nat) ) ). rewrite ( natsummationplusdistr ( S upper ) ( fun x0 : nat => hzquotientmod m x (a x0) * b (S upper - x0)%nat ) ). rewrite 2! hzplusassoc. apply ( maponpaths ( fun v => natsummation0 ( S upper ) ( fun i : nat => hzquotientmod m x ( a i ) * b ( sub ( S upper ) i ) ) + v ) ). rewrite ( hzqrandnatsummation0q m x ( fun i : nat => hzremaindermod m x ( a i ) * b ( sub ( S upper ) i ) ) ). assert (natsummation0 (S upper) (fun n : nat => hzremaindermod m x (hzremaindermod m x (a n) * b (S upper - n)%nat))= natsummation0 ( S upper ) ( fun n : nat => hzremaindermod m x ( a n * b ( sub ( S upper ) n ) ) ) ) as g. { apply natsummationpathsupperfixed. intros j p. rewrite hzremaindermodandtimes. rewrite hzremaindermoditerated. rewrite <- hzremaindermodandtimes. apply idpath. } rewrite g. rewrite <- hzplusassoc. assert ( natsummation0 (S upper) (fun x0 : nat => hzremaindermod m x (a x0) * hzquotientmod m x (b (S upper - x0)%nat)) + natsummation0 (S upper) (fun x0 : nat => hzquotientmod m x (hzremaindermod m x (a x0) * hzremaindermod m x (b (S upper - x0)%nat))) = natsummation0 (S upper) (fun n : nat => hzquotientmod m x (hzremaindermod m x (a n) * b (S upper - n)%nat)) ) as h. { rewrite <- ( natsummationplusdistr ( S upper ) ( fun x0 : nat => hzremaindermod m x ( a x0 ) * hzquotientmod m x ( b ( sub ( S upper ) x0 ) ) ) ). apply natsummationpathsupperfixed. intros j p. rewrite ( hzquotientmodandtimes m x ( hzremaindermod m x ( a j ) ) ( b ( sub ( S upper ) j ) ) ). rewrite <- hzqrandremainderq. rewrite 2! hzmult0x. rewrite hzmultx0. rewrite hzplusl0. rewrite hzremaindermoditerated. apply idpath. } rewrite h. apply idpath. 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.