proposition: Lemma finite_prod2 u v: finite_set u -> finite_set v -> finite_set (u \times v).
proof: Proof. move =>/NatP ha /NatP hb; apply /NatP. by rewrite - cprod2_pr1 - cprod2cl - cprod2cr; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)