proposition: Lemma ext_to_prod_bp A B C D f g: bijection_prop f A B -> bijection_prop g C D -> bijection_prop (f\ftimes g) (A \times C) (B\times D).
proof: Proof. move =>[bf <- <-][bg <- <-]. by move:(ext_to_prod_fb bf bg) => bb; split => //; rewrite/ext_to_prod; aw. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)