Lemma isapropisintdom (X : commring) : isaprop (isintdom X). Proof. use isapropdirprod. - apply propproperty. - use impred. intros x1. use impred. intros x2. use impred. intros H. use propproperty. Qed.
Require Import UniMath.Algebra.Groups.