proposition: Lemma ext_map_prod_VV x i: inc x (productf I src) -> inc i I -> Vg (Vf (ext_map_prod I src trg f) x) i = Vg (f i) (Vg x i) .
proof: Proof. move=> xp iI; rewrite ext_map_prod_V // LgV //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)