proposition: Lemma ocan_comp [fo : B -> option A] [ho : C -> option B] [f' : A -> B] [h' : B -> C] : ocancel fo f' -> ocancel ho h' -> ocancel (obind fo \o ho) (h' \o f').
proof: Proof. move=> fK hK c /=; rewrite -[RHS]hK/=; case hcE : (ho c) => [b|]//=. by rewrite -[b in RHS]fK; case: (fo b) => //=; have := hK c; rewrite hcE. Qed.
imports: ssreflect