proposition: Lemma Integers_infinite : ~ Finite nat Integers.
proof: Proof. generalize Integers_has_no_ub. intro H'; red; intro H'0; try exact H'0. apply H'. apply Finite_subset_has_lub; auto with sets arith. Qed.
imports: Finite_sets Constructive_sets Classical Classical_sets Powerset Powerset_facts Powerset_Classical_facts Finite_sets_facts Image Infinite_sets Compare_dec Relations_1 Partial_Order Cpo