# Library Coq.Sets.Integers

Require Export Finite_sets.
Require Export Constructive_sets.
Require Export Classical_Type.
Require Export Classical_sets.
Require Export Powerset.
Require Export Powerset_facts.
Require Export Powerset_Classical_facts.
Require Export Gt.
Require Export Lt.
Require Export Le.
Require Export Finite_sets_facts.
Require Export Image.
Require Export Infinite_sets.
Require Export Compare_dec.
Require Export Relations_1.
Require Export Partial_Order.
Require Export Cpo.
Section Integers_sect.
Inductive Integers : Ensemble nat :=
Integers_defn : forall x:nat, In nat Integers x.
Lemma le_reflexive : Reflexive nat le.
Lemma le_antisym : Antisymmetric nat le.
Lemma le_trans : Transitive nat le.
Lemma le_Order : Order nat le.
Lemma triv_nat : forall n:nat, In nat Integers n.
Definition nat_po : PO nat.
Defined.
Lemma le_total_order : Totally_ordered nat nat_po Integers.
Lemma Finite_subset_has_lub :
forall X:Ensemble nat,
Finite nat X -> exists m : nat, Upper_Bound nat nat_po X m.
Lemma Integers_has_no_ub :
~ (exists m : nat, Upper_Bound nat nat_po Integers m).
Lemma Integers_infinite : ~ Finite nat Integers.
End Integers_sect.