proposition: Lemma isapropinvpair (X : monoid) (x : X) : isaprop (invpair X x).
proof: Proof. intros. apply invproofirrelevance. intros x' x''. apply (invmaponpathsincl _ (isinclpr1 _ (λ a, isapropdirprod _ _ (setproperty X _ _) (setproperty X _ _)))). apply (pathslinvtorinv X x (invtolinv X x x') (invtorinv X x x'')). Defined.
imports: UniMath.Algebra.Groups UniMath.Algebra.RigsAndRings