Lemma isaprop_isDivRig (X : rig) : isaprop (isDivRig X). Proof. apply isofhleveldirprod. - now apply isapropneg. - apply impred_isaprop ; intro. apply isapropimpl. now apply isapropinvpair. Qed.
Require Import UniMath.MoreFoundations.Tactics.