Definition isasetfps ( R : commring ) : isaset ( seqson R ) := seqsonisaset R.
Require Import UniMath.PAdics.lemmas. Require Import UniMath.Algebra.RigsAndRings. Require Import UniMath.NumberSystems.Integers.