proposition: Lemma composable_pr f g: g \coP f -> (graph g) \cfP (graph f).
proof: Proof. move=> [fg ff st]; split; fprops. by rewrite domain_fg // st; apply: f_range_graph. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)