Lemma isrcancelablemonob {X Y : setwithbinop} (f : binopmono X Y) (x : X) (is : isrcancelable (@op Y) (f x)) : isrcancelable (@op X) x. Proof. unfold islcancelable. apply (isincltwooutof3a (λ x0 : X, op x0 x) f (pr2 (pr1 f))). assert (h : homot ((λ y0 : Y, op y0 (f x)) ∘ f) (f ∘ (λ x0 : X, op x0 x))). { intro x0; simpl. apply (!(pr2 f) x0 x). } apply (isinclhomot _ _ h). apply (isinclcomp f (make_incl _ is)). Defined.