Lemma isinvertiblemonof {X Y : setwithbinop} (f : binopiso X Y) (x : X) (is : isinvertible (@op X) x) : isinvertible (@op Y) (f x). Proof. apply (islinvertibleisof f x (pr1 is) ,, isrinvertibleisof f x (pr2 is)). Defined.