proposition: Lemma isapropmultinvpair : ∏ (X : rig) (x : X), isaprop (multinvpair X x).
proof: Proof. intros X x. apply isapropinvpair. Qed.
imports: UniMath.Algebra.Domains_and_Fields UniMath.Algebra.Monoids UniMath.Algebra.Groups