proposition: Lemma isinvoncarrier {X : gr} (A : subgr X) : isinv (@op A) (unel A) (λ a : A, make_carrier _ (grinv X (pr1 a)) (pr2 (pr2 A) (pr1 a) (pr2 a))).
proof: Proof. split. - intro a. apply (invmaponpathsincl _ (isinclpr1carrier A)). simpl. apply (grlinvax X (pr1 a)). - intro a. apply (invmaponpathsincl _ (isinclpr1carrier A)). simpl. apply (grrinvax X (pr1 a)). Defined.
imports: UniMath.MoreFoundations.Orders UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.Subtypes UniMath.Algebra.BinaryOperations UniMath.Algebra.Monoids