Lemma ismonoidopfpstimes ( R : commring ) : ismonoidop ( fpstimes R ). Proof. intros. unfold ismonoidop. split. - apply isassocfpstimes. - split with ( fpsone R). split. + intro s. unfold fpstimes. change ( ( fun n : nat => natsummation0 n ( fun x : nat => fpsone R x * s ( sub n x ) ) ) = s ). apply funextfun. intro n. destruct n. * simpl. rewrite ( ringlunax2 R ). apply idpath. * rewrite natsummationshift0. rewrite ( ringlunax2 R). rewrite minus0r. assert ( natsummation0 n ( fun x : nat => fpsone R ( S x ) * s ( sub n x ) ) = natsummation0 n ( fun x : nat => fpszero R x ) ) as f. { apply natsummationpathsupperfixed. intros m m'. rewrite ( ringmult0x R ). apply idpath. } change ( natsummation0 n ( fun x : nat => fpsone R ( S x ) * s ( sub n x ) ) + s ( S n ) = s ( S n ) ). rewrite f. rewrite natsummationandfpszero. apply ( ringlunax1 R ). + intros s. unfold fpstimes. change ( ( fun n : nat => natsummation0 n ( fun x : nat => s x * fpsone R ( sub n x ) ) ) = s ). apply funextfun. intro n. destruct n. * simpl. rewrite ( ringrunax2 R ). apply idpath. * change ( natsummation0 n ( fun x : nat => s x * fpsone R ( sub ( S n ) x ) ) + s ( S n ) * fpsone R ( sub n n ) = s ( S n ) ). rewrite minusnn0. rewrite ( ringrunax2 R ). assert ( natsummation0 n ( fun x : nat => s x * fpsone R ( sub ( S n ) x )) = ( natsummation0 n ( fun x : nat => fpszero R x ) ) ) as f. { apply natsummationpathsupperfixed. intros m m'. rewrite <- pathssminus. -- rewrite ( ringmultx0 R ). apply idpath. -- apply ( natlehlthtrans _ n ). ++ assumption. ++ apply natlthnsn. } rewrite f. rewrite natsummationandfpszero. apply ( ringlunax1 R ). Defined.
Require Import UniMath.PAdics.lemmas. Require Import UniMath.Algebra.RigsAndRings. Require Import UniMath.NumberSystems.Integers.