proposition: Lemma pc_VV x i: inc x (productb f) -> inc i (source u) -> Vg (Vf (product_compose f u) x) i = Vg x (Vf u i).
proof: Proof. move=> xp iu; rewrite pc_V //; move:(pc_axiom0 xp) => [fg -> ->] //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)