Lemma isinvisob {X Y : setwithbinop} (f : binopiso X Y) (uny : Y) (invy : Y → Y) (is : isinv (@op Y) uny invy) : isinv (@op X) (invmap (pr1 f) uny) (invmap f ∘ invy ∘ f). Proof. apply (isinvisof (invbinopiso f) uny invy is). Qed.