proposition: Theorem compf_f g f: g \coP f -> function (g \co f).
proof: Proof. move=> cgf; have cd:=(compf_domg cgf). have ac:=(composable_pr cgf). have fgcc:= (composef_fgraph (graph g) (graph f)). have cg := (compf_graph cgf); rewrite cg in cd. move: cg; rewrite /compose; aw => ->. have [fg ff etc] := cgf. apply: function_pr => //; last by rewrite cd domain_fg. apply: (sub_trans (composef_range ac)(f_range_graph fg)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)