proposition: Lemma infinite_Nat_alt: ~(finite_set Nat).
proof: Proof. move /NatP =>h. move: (sub_smaller (Nint_S (a:=\0c) (b:=cardinal Nat))). by rewrite (card_Nintc h); case /(cleSltP h). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)