proposition: Lemma cprod2_pr1 a b: a *c b = cardinal (a \times b).
proof: Proof. have bf:= (product2_canon_fb a b). symmetry;apply/card_eqP. by exists (product2_canon a b); split => //;rewrite/product2_canon; aw. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)