Lemma ismonoidopfpsplus ( R : commring ) : ismonoidop ( fpsplus R ). Proof. intros. unfold ismonoidop. split. - unfold isassoc. intros s t u. unfold fpsplus. change ( (fun n : nat => s n + t n + u n) = (fun n : nat => s n + (t n + u n)) ). apply funextfun. intro n. set ( H := pr2 R ). set ( H1 := pr1 H ). set ( H2 := pr1 H1 ). set ( H3 := pr1 H2 ). set ( H4 := pr1 H3 ). set ( H5 := pr1 H4 ). set ( H6 := pr1 H5 ). apply H6. - unfold isunital. assert ( isunit ( fpsplus R ) ( fpszero R ) ) as a. { unfold isunit. split. + unfold islunit. intro s. unfold fpsplus. unfold fpszero. change ( (fun n : nat => 0 + s n) = s ). apply funextfun. intro n. apply ringlunax1. + unfold isrunit. intro s. unfold fpsplus. unfold fpszero. change ( (fun n : nat => s n + 0) = s ). apply funextfun. intro n. apply ringrunax1. } exact ( tpair ( fpszero R ) a ). Defined.
Require Import UniMath.PAdics.lemmas. Require Import UniMath.Algebra.RigsAndRings. Require Import UniMath.NumberSystems.Integers.