proposition: Lemma isinvongrquot {X : gr} (R : binopeqrel X) : isinv (@op (setwithbinopquot R)) (setquotpr R (unel X)) (invongrquot R).
proof: Proof. split. - unfold islinv. apply (setquotunivprop R (λ x, _ = _)). intro x. apply (@maponpaths _ _ (setquotpr R) (@op X (grinv X x) x) (unel X)). apply (grlinvax X). - unfold isrinv. apply (setquotunivprop R (λ x, _ = _)). intro x. apply (@maponpaths _ _ (setquotpr R) (@op X x (grinv X x)) (unel X)). apply (grrinvax X). Defined.
imports: UniMath.MoreFoundations.Orders UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.Subtypes UniMath.Algebra.BinaryOperations UniMath.Algebra.Monoids