proposition: Lemma ext_to_prod_fun A B A' B' f g: inc f (functions A B) -> inc g (functions A' B') -> inc (f \ftimes g) (functions (A \times A') (B \times B')).
proof: Proof. move => /functionsP [ff sf tf] /functionsP [fg sg tg]. apply/functionsP; split. - by apply:ext_to_prod_f. - by rewrite /ext_to_prod; rewrite sf sg; aw. - by rewrite /ext_to_prod; rewrite tf tg; aw. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)