proposition: Lemma ext_to_prod_V2 c: inc c ((source u) \times (source v)) -> Vf (u \ftimes v) c = J (Vf u (P c)) (Vf v (Q c)).
proof: Proof. move => h;rewrite LfV // => t /setX_P [_ px py]; apply: setXp_i; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)