proposition: Lemma isapropisintdom (X : commring) : isaprop (isintdom X).
proof: Proof. use isapropdirprod. - apply propproperty. - use impred. intros x1. use impred. intros x2. use impred. intros H. use propproperty. Defined.
imports: UniMath.Algebra.Groups UniMath.Algebra.RigsAndRings