proposition: Lemma ext_to_prod_fb u v: bijection u -> bijection v -> bijection (u \ftimes v).
proof: Proof. move => [p1 p2] [p3 p4]. split; [by apply: ext_to_prod_fi | by apply: ext_to_prod_fs ]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)