proposition: Lemma prod_of_function_f x x': inc x (productb (graph f)) -> inc x' (productb (graph f')) -> inc (prod_of_fgraph x x') (productb (graph (prod_of_products f f'))).
proof: Proof. move=> xp x'p. move: (prod_of_products_f f f') => fp. move:(domain_fg ff) => eq1. move/setXb_P: (xp)=> [fgd dx]; rewrite eq1 => ivv. move/setXb_P: x'p=> [fgd' dx'] => ivv'. apply/setXb_P; rewrite (domain_fg fp) lf_source. rewrite /prod_of_fgraph; split; [ fprops | aw; ue | ]. move=> i idx; rewrite LgV //; last by rewrite dx eq1. rewrite -/(Vf _ _) (prod_of_products_V _ idx). apply:setXp_i; first by apply: (ivv i idx). by apply: ivv'; rewrite (domain_fg ff') - sfsf. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)