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