Library Coq.Sets.Integers

Require Export Finite_sets.
Require Export Constructive_sets.
Require Export Classical.
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.