proposition: Lemma ext_to_prod_bij A B A' B' f g: inc f (bijections A B) -> inc g (bijections A' B') -> inc (f \ftimes g) (bijections (A \times A') (B \times B')).
proof: Proof. move => /bijectionsP [ff sf tf] /bijectionsP [fg sg tg]. apply/bijectionsP; split. - by apply: ext_to_prod_fb. - 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)