proposition: Lemma bijective_ext_to_prod2C (a b a' b':Set) (u:a->a')(v:b->b'): bijectiveC u -> bijectiveC v -> bijectiveC (ext_to_prodC u v).
proof: Proof. rewrite /bijectiveC; move=> [p1 p2][p3 P4]. by split ; [apply: injective_ext_to_prod2C | apply: surjective_ext_to_prod2C]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)