proposition: Lemma prod_of_function_V x x' i: inc x (productb (graph f)) -> inc x' (productb (graph f')) -> inc i (source f) -> Vg (prod_of_fgraph x x') i = J (Vg x i) (Vg x' i).
proof: Proof. rewrite /prod_of_fgraph=> xp x'p isf; rewrite LgV //. by move/setXb_P: xp=> [_ -> _];rewrite domain_fg. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)