proposition: Lemma isinvertiblemonob {X Y : setwithbinop} (f : binopiso X Y) (x : X) (is : isinvertible (@op Y) (f x)) : isinvertible (@op X) x.
proof: Proof. apply (make_dirprod (islinvertibleisob f x (pr1 is)) (isrinvertibleisob f x (pr2 is))). Defined.
imports: UniMath.Foundations.Sets UniMath.MoreFoundations.Propositions