Lemma islinvertibleisob {X Y : setwithbinop} (f : binopiso X Y) (x : X) (is : islinvertible (@op Y) (f x)) : islinvertible (@op X) x. Proof. unfold islinvertible. apply (twooutof3a (λ x0 : X, op x x0) f). - assert (h : homot ((λ y0 : Y, op (f x) y0) ∘ f) (f ∘ (λ x0 : X, op x x0))). { intro x0; simpl. apply (!(pr2 f) x x0). } apply (isweqhomot _ _ h). apply (pr2 (weqcomp f (make_weq _ is))). - apply (pr2 (pr1 f)). Defined.