proposition: Lemma composef_range f g: f \cfP g -> sub (range (f \cf g)) (range f).
proof: Proof. move => [pa pb pc] t; move /(range_gP (composef_fgraph f g)) => [x]. rewrite composef_domain => xdg; rewrite (composef_ev _ xdg) => ->. apply /(range_gP pa); exists (Vg g x) => //. apply: pc; apply /(range_gP pb); ex_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)