Lemma iscancelablemonob {X Y : setwithbinop} (f : binopmono X Y) (x : X) (is : iscancelable (@op Y) (f x)) : iscancelable (@op X) x. Proof. apply (islcancelablemonob f x (pr1 is) ,, isrcancelablemonob f x (pr2 is)). Defined.