Lemma isassocfpstimes ( R : commring ) : isassoc (fpstimes R). Proof. intros. unfold isassoc. intros s t u. unfold fpstimes. assert ( (fun n : nat => natsummation0 n (fun x : nat => natsummation0 ( sub n x) (fun x0 : nat => s x * ( t x0 * u ( sub ( sub n x ) x0) )))) = (fun n : nat => natsummation0 n (fun x : nat => s x * natsummation0 ( sub n x) (fun x0 : nat => t x0 * u ( sub ( sub n x ) x0)))) ) as A. { apply funextfun. intro n. apply natsummationpathsupperfixed. intros. rewrite natsummationtimesdistr. apply idpath. } rewrite <- A. assert ( (fun n : nat => natsummation0 n (fun x : nat => natsummation0 ( sub n x) (fun x0 : nat => s x * t x0 * u ( sub ( sub n x ) x0 )))) = (fun n : nat => natsummation0 n (fun x : nat => natsummation0 ( sub n x) (fun x0 : nat => s x * ( t x0 * u ( sub ( sub n x ) x0) )))) ) as B. { apply funextfun. intro n. apply maponpaths. apply funextfun. intro m. apply maponpaths. apply funextfun. intro x. apply R. } assert ( (fun n : nat => natsummation0 n (fun x : nat => natsummation0 x (fun x0 : nat => s x0 * t ( sub x x0 ) * u ( sub n x )))) = (fun n : nat => natsummation0 n (fun x : nat => natsummation0 ( sub n x) (fun x0 : nat => s x * t x0 * u ( sub ( sub n x ) x0 )))) ) as C. { apply funextfun. intro n. set ( f := fun x : nat => ( fun x0 : nat => s x * t x0 * u ( sub ( sub n x ) x0 ) ) ). assert ( natsummation0 n ( fun x : nat => natsummation0 x ( fun x0 : nat => f x0 ( sub x x0 ) ) ) = natsummation0 n ( fun x : nat => natsummation0 ( sub n x ) ( fun x0 : nat => f x x0 ) ) ) as D by apply natsummationswap. unfold f in D. assert ( natsummation0 n ( fun x : nat => natsummation0 x ( fun x0 : nat => s x0 * t ( sub x x0 ) * u ( sub n x ) ) ) = natsummation0 n ( fun x : nat => natsummation0 x ( fun x0 : nat => s x0 * t ( sub x x0 ) * u ( sub ( sub n x0 ) ( sub x x0 ) ) ) ) ) as E. { apply natsummationpathsupperfixed. intros k p. apply natsummationpathsupperfixed. intros l q. rewrite ( natdoubleminus p q ). apply idpath. } rewrite E, D. apply idpath. } rewrite <- B. rewrite <- C. assert ( (fun n : nat => natsummation0 n (fun x : nat => natsummation0 x (fun x0 : nat => s x0 * t ( sub x x0)) * u ( sub n x))) = (fun n : nat => natsummation0 n (fun x : nat => natsummation0 x (fun x0 : nat => s x0 * t ( sub x x0) * u ( sub n x)))) ) as D. { apply funextfun. intro n. apply maponpaths. apply funextfun. intro m. apply natsummationtimesdistl. } rewrite <- D. apply idpath. Defined.
Require Import UniMath.PAdics.lemmas. Require Import UniMath.Algebra.RigsAndRings. Require Import UniMath.NumberSystems.Integers.