proposition: Lemma isaprop_isDivRig (X : rig) : isaprop (isDivRig X).
proof: Proof. apply isofhleveldirprod. - now apply isapropneg. - apply impred_isaprop ; intro. apply isapropimpl. now apply isapropinvpair. Qed.
imports: UniMath.Foundations.Sets UniMath.Algebra.RigsAndRings UniMath.Algebra.Domains_and_Fields UniMath.MoreFoundations.Tactics