Lemma isweqrmultingr_is {X : UU} {opp : binop X} (is : isgrop opp) (x0 : X) : isrinvertible opp x0. Proof. induction is as [ is istr ]. set (f := λ x : X, opp x x0). set (g := λ x : X, opp x ((pr1 istr) x0)). induction is as [ assoc isun0 ]. induction istr as [ inv0 axs ]. induction isun0 as [ un0 unaxs ]. simpl in * |-. assert (egf : ∏ x, g (f x) = x). { intro x. unfold f. unfold g. induction (!assoc x x0 (inv0 x0)). set (e := pr2 axs x0). simpl in e. rewrite e. apply (pr2 unaxs x). } assert (efg : ∏ x, f (g x) = x). { intro x. unfold f. unfold g. induction (!assoc x (inv0 x0) x0). set (e := pr1 axs x0). simpl in e. rewrite e. apply (pr2 unaxs x). } apply (isweq_iso _ _ egf efg). Defined.