proposition: Lemma ext_to_prod_fun_bis A B A' B' f g: function_prop f A B -> function_prop g A' B' -> function_prop (f \ftimes g) (A \times A') (B \times B').
proof: Proof. move => /functionsP ha /functionsP hb. by apply/functionsP /ext_to_prod_fun. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)