Definition acommringfps ( R : acommring ) : acommring. Proof. intros. split with ( fpscommring R ). split with ( fpsapart R ). split. - split. + apply ( fpsapartisbinopapartplusl R). + apply ( fpsapartisbinopapartplusr R ). - split. + apply ( fpsapartisbinopapartmultl R ). + apply ( fpsapartisbinopapartmultr R ). Defined.
Require Import UniMath.PAdics.lemmas. Require Import UniMath.Algebra.RigsAndRings. Require Import UniMath.NumberSystems.Integers.