Lemma isapropinvpair (X : monoid) (x : X) : isaprop (invpair X x). 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.
Require Import UniMath.Algebra.Groups.