Definition fpscommring ( R : commring ) : commring := make_commring ( fpsring R ) ( fpsiscommring R ).
Require Import UniMath.PAdics.lemmas. Require Import UniMath.Algebra.RigsAndRings. Require Import UniMath.NumberSystems.Integers.