proposition: Lemma isweqlmultingr_is {X : UU} {opp : binop X} (is : isgrop opp) (x0 : X) : islinvertible opp x0.
proof: Proof. destruct is as [ is istr ]. set (f := λ x : X, opp x0 x). set (g := λ x : X, opp ((pr1 istr) x0) x). destruct is as [ assoc isun0 ]. destruct istr as [ inv0 axs ]. destruct isun0 as [ un0 unaxs ]. simpl in * |-. assert (egf : ∏ x : _, paths (g (f x)) x). { intro x. unfold f. unfold g. destruct (assoc (inv0 x0) x0 x). set (e := pr1 axs x0). simpl in e. rewrite e. apply (pr1 unaxs x). } assert (efg : ∏ x : _, paths (f (g x)) x). { intro x. unfold f. unfold g. destruct (assoc x0 (inv0 x0) x). set (e := pr2 axs x0). simpl in e. rewrite e. apply (pr1 unaxs x). } apply (isweq_iso _ _ egf efg). Defined.
imports: UniMath.Foundations.Sets UniMath.MoreFoundations.Propositions