Lemma isgropfpsplus ( R : commring ) : isgrop ( fpsplus R ). Proof. intros. unfold isgrop. assert ( invstruct ( fpsplus R ) ( ismonoidopfpsplus R ) ) as a. { unfold invstruct. assert ( isinv (fpsplus R) (unel_is (ismonoidopfpsplus R)) ( fpsminus R ) ) as b. { unfold isinv. split. - unfold islinv. intro s. unfold fpsplus. unfold fpsminus. unfold unel_is. simpl. unfold fpszero. apply funextfun. intro n. exact ( ringlinvax1 R ( s n ) ). - unfold isrinv. intro s. unfold fpsplus. unfold fpsminus. unfold unel_is. simpl. unfold fpszero. apply funextfun. intro n. exact ( ringrinvax1 R ( s n ) ). } exact ( tpair ( fpsminus R ) b ). } exact ( tpair ( ismonoidopfpsplus R ) a ). Defined.
Require Import UniMath.PAdics.lemmas. Require Import UniMath.Algebra.RigsAndRings. Require Import UniMath.NumberSystems.Integers.