proposition: Lemma c3f_V u v f: function u -> function v -> function f -> source f = target u -> target f = source v -> Vf (compose3function u v) f = (v \co f) \co u.
proof: Proof. move => fu fv ff sf tf. rewrite LfV //; [apply: c3f_axiom=>// | by apply/functionsP]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)