Lemma isinvertiblemonob {X Y : setwithbinop} (f : binopiso X Y) (x : X) (is : isinvertible (@op Y) (f x)) : isinvertible (@op X) x. Proof. apply (islinvertibleisob f x (pr1 is) ,, isrinvertibleisob f x (pr2 is)). Defined.