Definition fpsring ( R : commring ) := make_setwith2binop ( make_hSet ( seqson R ) ( isasetfps R ) ) ( make_dirprod ( fpsplus R ) ( fpstimes R ) ).
Require Import UniMath.PAdics.lemmas. Require Import UniMath.Algebra.RigsAndRings. Require Import UniMath.NumberSystems.Integers.