proposition: Theorem fpsiscommring ( R : commring ) : iscommring ( fpsring R ).
proof: Proof. unfold iscommring. unfold iscommringops. split. - unfold isringops. split. + split. * unfold isabgrop. -- split. ++ exact ( isgropfpsplus R ). ++ exact ( iscommfpsplus R ). * exact ( ismonoidopfpstimes R ). + unfold isdistr. * split. -- unfold isldistr. intros. apply ( isldistrfps R ). -- unfold isrdistr. intros. apply ( isrdistrfps R ). - unfold iscomm. intros. apply ( iscommfpstimes R ). Defined.
imports: UniMath.PAdics.lemmas UniMath.Algebra.RigsAndRings UniMath.NumberSystems.Integers