Lemma iscommfpstimes ( R : commring ) ( s t : fps R ) : fpstimes R s t = fpstimes R t s. Proof. intros. unfold fpstimes. change ( ( fun n : nat => natsummation0 n (fun x : nat => s x * t ( sub n x) ) ) = ( fun n : nat => natsummation0 n (fun x : nat => t x * s ( sub n x) ) ) ). apply funextfun. intro n. assert ( natsummation0 n ( fun x : nat => s x * t ( sub n x ) ) = natsummation0 n ( fun x : nat => t ( sub n x ) * s x ) ) as a0. { apply maponpaths. apply funextfun. intro m. apply R. } assert ( ( natsummation0 n ( fun x : nat => t ( sub n x ) * s x ) ) = natsummation0 n ( funcomp ( nattruncreverse n ) ( fun x : nat => t x * s ( sub n x ) ) ) ) as a1. { apply natsummationpathsupperfixed. intros m q. unfold funcomp. unfold nattruncreverse. destruct (natgthorleh m n ). - apply fromempty. apply isirreflnatlth with ( n := n ). apply natlthlehtrans with ( m := m ). + apply h. + assumption. - apply maponpaths. apply maponpaths. apply pathsinv0. apply doubleminuslehpaths. assumption. } assert ( natsummation0 n ( funcomp ( nattruncreverse n ) ( fun x : nat => t x * s ( sub n x ) ) ) = natsummation0 n ( fun x : nat => t x * s ( sub n x ) ) ) as a2. { apply pathsinv0. apply natsummationreindexing. apply nattruncreverseisnattruncauto. } exact ( pathscomp0 a0 ( pathscomp0 a1 a2 ) ). Defined.
Require Import UniMath.PAdics.lemmas. Require Import UniMath.Algebra.RigsAndRings. Require Import UniMath.NumberSystems.Integers.