proposition: Lemma iscancelablemonob {X Y : setwithbinop} (f : binopmono X Y) (x : X) (is : iscancelable (@op Y) (f x)) : iscancelable (@op X) x.
proof: Proof. apply (make_dirprod (islcancelablemonob f x (pr1 is)) (isrcancelablemonob f x (pr2 is))). Defined.
imports: UniMath.Foundations.Sets UniMath.MoreFoundations.Propositions