proposition: Lemma pcan_in_comp [A B C : Type] (D : {pred B}) (D' : {pred C}) [f : B -> A] [h : C -> B] [f' : A -> option B] [h' : B -> option C] : {homo h : x / x \in D' >-> x \in D} -> {in D, pcancel f f'} -> {in D', pcancel h h'} -> {in D', pcancel (f \o h) (obind h' \o f')}.
proof: Proof. by move=> hD fK hK c cD /=; rewrite fK/= ?hK ?hD. Qed.
imports: ssreflect ssrfun