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
.