proposition: Lemma compf_graph: {when: composable, {morph graph: f g / f \co g >-> f \cf g}}.
proof: Proof. move => a b cfg; move:(composable_pr cfg)=> ac. by rewrite /compose compg_composef; aw. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)