proposition: Lemma compose_ext_to_prod2 u v u' v': u' \coP u -> v' \coP v -> (u'\ftimes v') \co (u \ftimes v) = (u' \co u) \ftimes (v' \co v).
proof: Proof. move=> cuu cvv. move:(ext_to_prod_coP cuu cvv) => cee. have fcu: (function (u' \co u)) by fct_tac. have fcv: (function (v' \co v)) by fct_tac. apply: function_exten. - fct_tac. - fprops. - by rewrite/ext_to_prod;aw. - by rewrite/ext_to_prod;aw. - aw; move => x xs1; move: (xs1); rewrite ext_to_prod_s => xs. move:(xs); move/setX_P => [xp pxs qxs]. have res1: inc (Vf (ext_to_prod u v) x) (product (source u') (source v')). have aux: (product (source u') (source v')= target(ext_to_prod u v)). by move:cuu => [_ _ ->]; move: cvv => [_ _ ->]; rewrite /ext_to_prod; aw. Wtac; fct_tac. rewrite compfV // ext_to_prod_V2 //; try fct_tac. rewrite ext_to_prod_V2 //; try fct_tac. by rewrite ext_to_prod_V2 //; [ rewrite !compfV //; aw | aw]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)