Theorem fpsiscommring ( R : commring ) : iscommring ( fpsring R ). 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.
Require Import UniMath.PAdics.lemmas. Require Import UniMath.Algebra.RigsAndRings. Require Import UniMath.NumberSystems.Integers.