Integers.v

Built with Alectryon, running Coq+SerAPI v8.10.0+0.7.0. Coq sources are in this panel; goals and messages will appear in the other. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus.
(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)
(****************************************************************************)
(*                                                                          *)
(*                         Naive Set Theory in Coq                          *)
(*                                                                          *)
(*                     INRIA                        INRIA                   *)
(*              Rocquencourt                        Sophia-Antipolis        *)
(*                                                                          *)
(*                                 Coq V6.1                                 *)
(*									    *)
(*			         Gilles Kahn 				    *)
(*				 Gerard Huet				    *)
(*									    *)
(*									    *)
(*                                                                          *)
(* Acknowledgments: This work was started in July 1993 by F. Prost. Thanks  *)
(* to the Newton Institute for providing an exceptional work environment    *)
(* in Summer 1995. Several developments by E. Ledinot were an inspiration.  *)
(****************************************************************************)

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.Reflexive nat le
  Proof.Reflexive nat le
    red; auto with arith.
  Qed.

  Lemma le_antisym : Antisymmetric nat le.Antisymmetric nat le
  Proof.Antisymmetric nat le
    red; intros x y H H'; rewrite (le_antisym x y); auto.
  Qed.

  Lemma le_trans : Transitive nat le.Transitive nat le
  Proof.Transitive nat le
    red; intros; apply le_trans with y; auto.
  Qed.

  Lemma le_Order : Order nat le.Order nat le
  Proof.Order nat le
    split; [exact le_reflexive | exact le_trans | exact le_antisym].
  Qed.

  Lemma triv_nat : forall n:nat, In nat Integers n.forall n : nat, In nat Integers n
  Proof.forall n : nat, In nat Integers n
    exact Integers_defn.
  Qed.

  Definition nat_po : PO nat.PO nat
    apply Definition_of_PO with (Carrier_of := Integers) (Rel_of := le);
      auto with sets arith.Inhabited nat Integers
Order nat le
    apply Inhabited_intro with (x := 0).In nat Integers 0
Order nat le
      apply Integers_defn.Order nat le
    exact le_Order.
  Defined.

  Lemma le_total_order : Totally_ordered nat nat_po Integers.Totally_ordered nat nat_po Integers
  Proof.Totally_ordered nat nat_po Integers
    apply Totally_ordered_definition.Included nat Integers (Carrier_of nat nat_po) ->
forall x y : nat,
Included nat (Couple nat x y) Integers ->
Rel_of nat nat_po x y \/ Rel_of nat nat_po y x
    simpl.Included nat Integers Integers ->
forall x y : nat,
Included nat (Couple nat x y) Integers ->
x <= y \/ y <= x
    intros H' x y H'0.H':Included nat Integers Integers
x, y:nat
H'0:Included nat (Couple nat x y) Integers
x <= y \/ y <= x
    elim le_or_lt with (n := x) (m := y).H':Included nat Integers Integers
x, y:nat
H'0:Included nat (Couple nat x y) Integers
x <= y -> x <= y \/ y <= x
H':Included nat Integers Integers
x, y:nat
H'0:Included nat (Couple nat x y) Integers
y < x -> x <= y \/ y <= x
    intro H'1; left; auto with sets arith.H':Included nat Integers Integers
x, y:nat
H'0:Included nat (Couple nat x y) Integers
y < x -> x <= y \/ y <= x
    intro H'1; right.H':Included nat Integers Integers
x, y:nat
H'0:Included nat (Couple nat x y) Integers
H'1:y < x
y <= x
    cut (y <= x); auto with sets arith.
  Qed.

  Lemma Finite_subset_has_lub :
    forall X:Ensemble nat,
      Finite nat X ->  exists m : nat, Upper_Bound nat nat_po X m.forall X : Ensemble nat,
Finite nat X ->
exists m : nat, Upper_Bound nat nat_po X m
  Proof.forall X : Ensemble nat,
Finite nat X ->
exists m : nat, Upper_Bound nat nat_po X m
    intros X H'; elim H'.X:Ensemble nat
H':Finite nat X
exists m : nat,
  Upper_Bound nat nat_po (Empty_set nat) m
X:Ensemble nat
H':Finite nat X
forall A : Ensemble nat,
Finite nat A ->
(exists m : nat, Upper_Bound nat nat_po A m) ->
forall x : nat,
~ In nat A x ->
exists m : nat, Upper_Bound nat nat_po (Add nat A x) m
    exists 0.X:Ensemble nat
H':Finite nat X
Upper_Bound nat nat_po (Empty_set nat) 0
X:Ensemble nat
H':Finite nat X
forall A : Ensemble nat,
Finite nat A ->
(exists m : nat, Upper_Bound nat nat_po A m) ->
forall x : nat,
~ In nat A x ->
exists m : nat, Upper_Bound nat nat_po (Add nat A x) m
    apply Upper_Bound_definition.X:Ensemble nat
H':Finite nat X
In nat (Carrier_of nat nat_po) 0
X:Ensemble nat
H':Finite nat X
forall y : nat,
In nat (Empty_set nat) y -> Rel_of nat nat_po y 0
X:Ensemble nat
H':Finite nat X
forall A : Ensemble nat,
Finite nat A ->
(exists m : nat, Upper_Bound nat nat_po A m) ->
forall x : nat,
~ In nat A x ->
exists m : nat, Upper_Bound nat nat_po (Add nat A x) m
      unfold nat_po.X:Ensemble nat
H':Finite nat X
In nat
  (Carrier_of nat
     {|
     Carrier_of := Integers;
     Rel_of := le;
     PO_cond1 := Inhabited_intro nat Integers 0
                   (Integers_defn 0);
     PO_cond2 := le_Order |}) 0
X:Ensemble nat
H':Finite nat X
forall y : nat,
In nat (Empty_set nat) y -> Rel_of nat nat_po y 0
X:Ensemble nat
H':Finite nat X
forall A : Ensemble nat,
Finite nat A ->
(exists m : nat, Upper_Bound nat nat_po A m) ->
forall x : nat,
~ In nat A x ->
exists m : nat, Upper_Bound nat nat_po (Add nat A x) m simpl.X:Ensemble nat
H':Finite nat X
In nat Integers 0
X:Ensemble nat
H':Finite nat X
forall y : nat,
In nat (Empty_set nat) y -> Rel_of nat nat_po y 0
X:Ensemble nat
H':Finite nat X
forall A : Ensemble nat,
Finite nat A ->
(exists m : nat, Upper_Bound nat nat_po A m) ->
forall x : nat,
~ In nat A x ->
exists m : nat, Upper_Bound nat nat_po (Add nat A x) m apply triv_nat.X:Ensemble nat
H':Finite nat X
forall y : nat,
In nat (Empty_set nat) y -> Rel_of nat nat_po y 0
X:Ensemble nat
H':Finite nat X
forall A : Ensemble nat,
Finite nat A ->
(exists m : nat, Upper_Bound nat nat_po A m) ->
forall x : nat,
~ In nat A x ->
exists m : nat, Upper_Bound nat nat_po (Add nat A x) m
    intros y H'0; elim H'0; auto with sets arith.X:Ensemble nat
H':Finite nat X
forall A : Ensemble nat,
Finite nat A ->
(exists m : nat, Upper_Bound nat nat_po A m) ->
forall x : nat,
~ In nat A x ->
exists m : nat, Upper_Bound nat nat_po (Add nat A x) m
    intros A H'0 H'1 x H'2; try assumption.X:Ensemble nat
H':Finite nat X
A:Ensemble nat
H'0:Finite nat A
H'1:exists m : nat, Upper_Bound nat nat_po A m
x:nat
H'2:~ In nat A x
exists m : nat, Upper_Bound nat nat_po (Add nat A x) m
    elim H'1; intros x0 H'3; clear H'1.X:Ensemble nat
H':Finite nat X
A:Ensemble nat
H'0:Finite nat A
x:nat
H'2:~ In nat A x
x0:nat
H'3:Upper_Bound nat nat_po A x0
exists m : nat, Upper_Bound nat nat_po (Add nat A x) m
    elim le_total_order.X:Ensemble nat
H':Finite nat X
A:Ensemble nat
H'0:Finite nat A
x:nat
H'2:~ In nat A x
x0:nat
H'3:Upper_Bound nat nat_po A x0
(Included nat Integers (Carrier_of nat nat_po) ->
 forall x1 y : nat,
 Included nat (Couple nat x1 y) Integers ->
 Rel_of nat nat_po x1 y \/ Rel_of nat nat_po y x1) ->
exists m : nat, Upper_Bound nat nat_po (Add nat A x) m
    simpl.X:Ensemble nat
H':Finite nat X
A:Ensemble nat
H'0:Finite nat A
x:nat
H'2:~ In nat A x
x0:nat
H'3:Upper_Bound nat nat_po A x0
(Included nat Integers Integers ->
 forall x1 y : nat,
 Included nat (Couple nat x1 y) Integers ->
 x1 <= y \/ y <= x1) ->
exists m : nat, Upper_Bound nat nat_po (Add nat A x) m
    intro H'1; try assumption.X:Ensemble nat
H':Finite nat X
A:Ensemble nat
H'0:Finite nat A
x:nat
H'2:~ In nat A x
x0:nat
H'3:Upper_Bound nat nat_po A x0
H'1:Included nat Integers Integers ->
forall x1 y : nat,
Included nat (Couple nat x1 y) Integers -> x1 <= y \/ y <= x1
exists m : nat, Upper_Bound nat nat_po (Add nat A x) m
    lapply H'1; [ intro H'4; idtac | try assumption ]; auto with sets arith.X:Ensemble nat
H':Finite nat X
A:Ensemble nat
H'0:Finite nat A
x:nat
H'2:~ In nat A x
x0:nat
H'3:Upper_Bound nat nat_po A x0
H'1:Included nat Integers Integers ->
forall x1 y : nat,
Included nat (Couple nat x1 y) Integers -> x1 <= y \/ y <= x1
H'4:forall x1 y : nat,
Included nat (Couple nat x1 y) Integers -> x1 <= y \/ y <= x1
exists m : nat, Upper_Bound nat nat_po (Add nat A x) m
    generalize (H'4 x0 x).X:Ensemble nat
H':Finite nat X
A:Ensemble nat
H'0:Finite nat A
x:nat
H'2:~ In nat A x
x0:nat
H'3:Upper_Bound nat nat_po A x0
H'1:Included nat Integers Integers ->
forall x1 y : nat,
Included nat (Couple nat x1 y) Integers -> x1 <= y \/ y <= x1
H'4:forall x1 y : nat,
Included nat (Couple nat x1 y) Integers -> x1 <= y \/ y <= x1
(Included nat (Couple nat x0 x) Integers ->
 x0 <= x \/ x <= x0) ->
exists m : nat, Upper_Bound nat nat_po (Add nat A x) m
    clear H'4.X:Ensemble nat
H':Finite nat X
A:Ensemble nat
H'0:Finite nat A
x:nat
H'2:~ In nat A x
x0:nat
H'3:Upper_Bound nat nat_po A x0
H'1:Included nat Integers Integers ->
forall x1 y : nat,
Included nat (Couple nat x1 y) Integers -> x1 <= y \/ y <= x1
(Included nat (Couple nat x0 x) Integers ->
 x0 <= x \/ x <= x0) ->
exists m : nat, Upper_Bound nat nat_po (Add nat A x) m
    clear H'1.X:Ensemble nat
H':Finite nat X
A:Ensemble nat
H'0:Finite nat A
x:nat
H'2:~ In nat A x
x0:nat
H'3:Upper_Bound nat nat_po A x0
(Included nat (Couple nat x0 x) Integers ->
 x0 <= x \/ x <= x0) ->
exists m : nat, Upper_Bound nat nat_po (Add nat A x) m
    intro H'1; lapply H'1;
      [ intro H'4; elim H'4;
	[ intro H'5; try exact H'5; clear H'4 H'1 | intro H'5; clear H'4 H'1 ]
	| clear H'1 ].X:Ensemble nat
H':Finite nat X
A:Ensemble nat
H'0:Finite nat A
x:nat
H'2:~ In nat A x
x0:nat
H'3:Upper_Bound nat nat_po A x0
H'5:x0 <= x
exists m : nat, Upper_Bound nat nat_po (Add nat A x) m
X:Ensemble nat
H':Finite nat X
A:Ensemble nat
H'0:Finite nat A
x:nat
H'2:~ In nat A x
x0:nat
H'3:Upper_Bound nat nat_po A x0
H'5:x <= x0
exists m : nat, Upper_Bound nat nat_po (Add nat A x) m
X:Ensemble nat
H':Finite nat X
A:Ensemble nat
H'0:Finite nat A
x:nat
H'2:~ In nat A x
x0:nat
H'3:Upper_Bound nat nat_po A x0
Included nat (Couple nat x0 x) Integers
    exists x.X:Ensemble nat
H':Finite nat X
A:Ensemble nat
H'0:Finite nat A
x:nat
H'2:~ In nat A x
x0:nat
H'3:Upper_Bound nat nat_po A x0
H'5:x0 <= x
Upper_Bound nat nat_po (Add nat A x) x
X:Ensemble nat
H':Finite nat X
A:Ensemble nat
H'0:Finite nat A
x:nat
H'2:~ In nat A x
x0:nat
H'3:Upper_Bound nat nat_po A x0
H'5:x <= x0
exists m : nat, Upper_Bound nat nat_po (Add nat A x) m
X:Ensemble nat
H':Finite nat X
A:Ensemble nat
H'0:Finite nat A
x:nat
H'2:~ In nat A x
x0:nat
H'3:Upper_Bound nat nat_po A x0
Included nat (Couple nat x0 x) Integers
    apply Upper_Bound_definition.X:Ensemble nat
H':Finite nat X
A:Ensemble nat
H'0:Finite nat A
x:nat
H'2:~ In nat A x
x0:nat
H'3:Upper_Bound nat nat_po A x0
H'5:x0 <= x
In nat (Carrier_of nat nat_po) x
X:Ensemble nat
H':Finite nat X
A:Ensemble nat
H'0:Finite nat A
x:nat
H'2:~ In nat A x
x0:nat
H'3:Upper_Bound nat nat_po A x0
H'5:x0 <= x
forall y : nat,
In nat (Add nat A x) y -> Rel_of nat nat_po y x
X:Ensemble nat
H':Finite nat X
A:Ensemble nat
H'0:Finite nat A
x:nat
H'2:~ In nat A x
x0:nat
H'3:Upper_Bound nat nat_po A x0
H'5:x <= x0
exists m : nat, Upper_Bound nat nat_po (Add nat A x) m
X:Ensemble nat
H':Finite nat X
A:Ensemble nat
H'0:Finite nat A
x:nat
H'2:~ In nat A x
x0:nat
H'3:Upper_Bound nat nat_po A x0
Included nat (Couple nat x0 x) Integers simpl.X:Ensemble nat
H':Finite nat X
A:Ensemble nat
H'0:Finite nat A
x:nat
H'2:~ In nat A x
x0:nat
H'3:Upper_Bound nat nat_po A x0
H'5:x0 <= x
In nat Integers x
X:Ensemble nat
H':Finite nat X
A:Ensemble nat
H'0:Finite nat A
x:nat
H'2:~ In nat A x
x0:nat
H'3:Upper_Bound nat nat_po A x0
H'5:x0 <= x
forall y : nat,
In nat (Add nat A x) y -> Rel_of nat nat_po y x
X:Ensemble nat
H':Finite nat X
A:Ensemble nat
H'0:Finite nat A
x:nat
H'2:~ In nat A x
x0:nat
H'3:Upper_Bound nat nat_po A x0
H'5:x <= x0
exists m : nat, Upper_Bound nat nat_po (Add nat A x) m
X:Ensemble nat
H':Finite nat X
A:Ensemble nat
H'0:Finite nat A
x:nat
H'2:~ In nat A x
x0:nat
H'3:Upper_Bound nat nat_po A x0
Included nat (Couple nat x0 x) Integers apply triv_nat.X:Ensemble nat
H':Finite nat X
A:Ensemble nat
H'0:Finite nat A
x:nat
H'2:~ In nat A x
x0:nat
H'3:Upper_Bound nat nat_po A x0
H'5:x0 <= x
forall y : nat,
In nat (Add nat A x) y -> Rel_of nat nat_po y x
X:Ensemble nat
H':Finite nat X
A:Ensemble nat
H'0:Finite nat A
x:nat
H'2:~ In nat A x
x0:nat
H'3:Upper_Bound nat nat_po A x0
H'5:x <= x0
exists m : nat, Upper_Bound nat nat_po (Add nat A x) m
X:Ensemble nat
H':Finite nat X
A:Ensemble nat
H'0:Finite nat A
x:nat
H'2:~ In nat A x
x0:nat
H'3:Upper_Bound nat nat_po A x0
Included nat (Couple nat x0 x) Integers
    intros y H'1; elim H'1.X:Ensemble nat
H':Finite nat X
A:Ensemble nat
H'0:Finite nat A
x:nat
H'2:~ In nat A x
x0:nat
H'3:Upper_Bound nat nat_po A x0
H'5:x0 <= x
y:nat
H'1:In nat (Add nat A x) y
forall x1 : nat, In nat A x1 -> Rel_of nat nat_po x1 x
X:Ensemble nat
H':Finite nat X
A:Ensemble nat
H'0:Finite nat A
x:nat
H'2:~ In nat A x
x0:nat
H'3:Upper_Bound nat nat_po A x0
H'5:x0 <= x
y:nat
H'1:In nat (Add nat A x) y
forall x1 : nat,
In nat (Singleton nat x) x1 -> Rel_of nat nat_po x1 x
X:Ensemble nat
H':Finite nat X
A:Ensemble nat
H'0:Finite nat A
x:nat
H'2:~ In nat A x
x0:nat
H'3:Upper_Bound nat nat_po A x0
H'5:x <= x0
exists m : nat, Upper_Bound nat nat_po (Add nat A x) m
X:Ensemble nat
H':Finite nat X
A:Ensemble nat
H'0:Finite nat A
x:nat
H'2:~ In nat A x
x0:nat
H'3:Upper_Bound nat nat_po A x0
Included nat (Couple nat x0 x) Integers
    generalize le_trans.X:Ensemble nat
H':Finite nat X
A:Ensemble nat
H'0:Finite nat A
x:nat
H'2:~ In nat A x
x0:nat
H'3:Upper_Bound nat nat_po A x0
H'5:x0 <= x
y:nat
H'1:In nat (Add nat A x) y
Transitive nat le ->
forall x1 : nat, In nat A x1 -> Rel_of nat nat_po x1 x
X:Ensemble nat
H':Finite nat X
A:Ensemble nat
H'0:Finite nat A
x:nat
H'2:~ In nat A x
x0:nat
H'3:Upper_Bound nat nat_po A x0
H'5:x0 <= x
y:nat
H'1:In nat (Add nat A x) y
forall x1 : nat,
In nat (Singleton nat x) x1 -> Rel_of nat nat_po x1 x
X:Ensemble nat
H':Finite nat X
A:Ensemble nat
H'0:Finite nat A
x:nat
H'2:~ In nat A x
x0:nat
H'3:Upper_Bound nat nat_po A x0
H'5:x <= x0
exists m : nat, Upper_Bound nat nat_po (Add nat A x) m
X:Ensemble nat
H':Finite nat X
A:Ensemble nat
H'0:Finite nat A
x:nat
H'2:~ In nat A x
x0:nat
H'3:Upper_Bound nat nat_po A x0
Included nat (Couple nat x0 x) Integers
    intro H'4; red in H'4.X:Ensemble nat
H':Finite nat X
A:Ensemble nat
H'0:Finite nat A
x:nat
H'2:~ In nat A x
x0:nat
H'3:Upper_Bound nat nat_po A x0
H'5:x0 <= x
y:nat
H'1:In nat (Add nat A x) y
H'4:forall x1 y0 z : nat, x1 <= y0 -> y0 <= z -> x1 <= z
forall x1 : nat, In nat A x1 -> Rel_of nat nat_po x1 x
X:Ensemble nat
H':Finite nat X
A:Ensemble nat
H'0:Finite nat A
x:nat
H'2:~ In nat A x
x0:nat
H'3:Upper_Bound nat nat_po A x0
H'5:x0 <= x
y:nat
H'1:In nat (Add nat A x) y
forall x1 : nat,
In nat (Singleton nat x) x1 -> Rel_of nat nat_po x1 x
X:Ensemble nat
H':Finite nat X
A:Ensemble nat
H'0:Finite nat A
x:nat
H'2:~ In nat A x
x0:nat
H'3:Upper_Bound nat nat_po A x0
H'5:x <= x0
exists m : nat, Upper_Bound nat nat_po (Add nat A x) m
X:Ensemble nat
H':Finite nat X
A:Ensemble nat
H'0:Finite nat A
x:nat
H'2:~ In nat A x
x0:nat
H'3:Upper_Bound nat nat_po A x0
Included nat (Couple nat x0 x) Integers
    intros x1 H'6; try assumption.X:Ensemble nat
H':Finite nat X
A:Ensemble nat
H'0:Finite nat A
x:nat
H'2:~ In nat A x
x0:nat
H'3:Upper_Bound nat nat_po A x0
H'5:x0 <= x
y:nat
H'1:In nat (Add nat A x) y
H'4:forall x2 y0 z : nat, x2 <= y0 -> y0 <= z -> x2 <= z
x1:nat
H'6:In nat A x1
Rel_of nat nat_po x1 x
X:Ensemble nat
H':Finite nat X
A:Ensemble nat
H'0:Finite nat A
x:nat
H'2:~ In nat A x
x0:nat
H'3:Upper_Bound nat nat_po A x0
H'5:x0 <= x
y:nat
H'1:In nat (Add nat A x) y
forall x1 : nat,
In nat (Singleton nat x) x1 -> Rel_of nat nat_po x1 x
X:Ensemble nat
H':Finite nat X
A:Ensemble nat
H'0:Finite nat A
x:nat
H'2:~ In nat A x
x0:nat
H'3:Upper_Bound nat nat_po A x0
H'5:x <= x0
exists m : nat, Upper_Bound nat nat_po (Add nat A x) m
X:Ensemble nat
H':Finite nat X
A:Ensemble nat
H'0:Finite nat A
x:nat
H'2:~ In nat A x
x0:nat
H'3:Upper_Bound nat nat_po A x0
Included nat (Couple nat x0 x) Integers
    apply H'4 with (y := x0).X:Ensemble nat
H':Finite nat X
A:Ensemble nat
H'0:Finite nat A
x:nat
H'2:~ In nat A x
x0:nat
H'3:Upper_Bound nat nat_po A x0
H'5:x0 <= x
y:nat
H'1:In nat (Add nat A x) y
H'4:forall x2 y0 z : nat, x2 <= y0 -> y0 <= z -> x2 <= z
x1:nat
H'6:In nat A x1
x1 <= x0
X:Ensemble nat
H':Finite nat X
A:Ensemble nat
H'0:Finite nat A
x:nat
H'2:~ In nat A x
x0:nat
H'3:Upper_Bound nat nat_po A x0
H'5:x0 <= x
y:nat
H'1:In nat (Add nat A x) y
H'4:forall x2 y0 z : nat, x2 <= y0 -> y0 <= z -> x2 <= z
x1:nat
H'6:In nat A x1
x0 <= x
X:Ensemble nat
H':Finite nat X
A:Ensemble nat
H'0:Finite nat A
x:nat
H'2:~ In nat A x
x0:nat
H'3:Upper_Bound nat nat_po A x0
H'5:x0 <= x
y:nat
H'1:In nat (Add nat A x) y
forall x1 : nat,
In nat (Singleton nat x) x1 -> Rel_of nat nat_po x1 x
X:Ensemble nat
H':Finite nat X
A:Ensemble nat
H'0:Finite nat A
x:nat
H'2:~ In nat A x
x0:nat
H'3:Upper_Bound nat nat_po A x0
H'5:x <= x0
exists m : nat, Upper_Bound nat nat_po (Add nat A x) m
X:Ensemble nat
H':Finite nat X
A:Ensemble nat
H'0:Finite nat A
x:nat
H'2:~ In nat A x
x0:nat
H'3:Upper_Bound nat nat_po A x0
Included nat (Couple nat x0 x) Integers elim H'3; simpl; auto with sets arith.X:Ensemble nat
H':Finite nat X
A:Ensemble nat
H'0:Finite nat A
x:nat
H'2:~ In nat A x
x0:nat
H'3:Upper_Bound nat nat_po A x0
H'5:x0 <= x
y:nat
H'1:In nat (Add nat A x) y
H'4:forall x2 y0 z : nat, x2 <= y0 -> y0 <= z -> x2 <= z
x1:nat
H'6:In nat A x1
x0 <= x
X:Ensemble nat
H':Finite nat X
A:Ensemble nat
H'0:Finite nat A
x:nat
H'2:~ In nat A x
x0:nat
H'3:Upper_Bound nat nat_po A x0
H'5:x0 <= x
y:nat
H'1:In nat (Add nat A x) y
forall x1 : nat,
In nat (Singleton nat x) x1 -> Rel_of nat nat_po x1 x
X:Ensemble nat
H':Finite nat X
A:Ensemble nat
H'0:Finite nat A
x:nat
H'2:~ In nat A x
x0:nat
H'3:Upper_Bound nat nat_po A x0
H'5:x <= x0
exists m : nat, Upper_Bound nat nat_po (Add nat A x) m
X:Ensemble nat
H':Finite nat X
A:Ensemble nat
H'0:Finite nat A
x:nat
H'2:~ In nat A x
x0:nat
H'3:Upper_Bound nat nat_po A x0
Included nat (Couple nat x0 x) Integers trivial.X:Ensemble nat
H':Finite nat X
A:Ensemble nat
H'0:Finite nat A
x:nat
H'2:~ In nat A x
x0:nat
H'3:Upper_Bound nat nat_po A x0
H'5:x0 <= x
y:nat
H'1:In nat (Add nat A x) y
forall x1 : nat,
In nat (Singleton nat x) x1 -> Rel_of nat nat_po x1 x
X:Ensemble nat
H':Finite nat X
A:Ensemble nat
H'0:Finite nat A
x:nat
H'2:~ In nat A x
x0:nat
H'3:Upper_Bound nat nat_po A x0
H'5:x <= x0
exists m : nat, Upper_Bound nat nat_po (Add nat A x) m
X:Ensemble nat
H':Finite nat X
A:Ensemble nat
H'0:Finite nat A
x:nat
H'2:~ In nat A x
x0:nat
H'3:Upper_Bound nat nat_po A x0
Included nat (Couple nat x0 x) Integers
    intros x1 H'4; elim H'4.X:Ensemble nat
H':Finite nat X
A:Ensemble nat
H'0:Finite nat A
x:nat
H'2:~ In nat A x
x0:nat
H'3:Upper_Bound nat nat_po A x0
H'5:x0 <= x
y:nat
H'1:In nat (Add nat A x) y
x1:nat
H'4:In nat (Singleton nat x) x1
Rel_of nat nat_po x x
X:Ensemble nat
H':Finite nat X
A:Ensemble nat
H'0:Finite nat A
x:nat
H'2:~ In nat A x
x0:nat
H'3:Upper_Bound nat nat_po A x0
H'5:x <= x0
exists m : nat, Upper_Bound nat nat_po (Add nat A x) m
X:Ensemble nat
H':Finite nat X
A:Ensemble nat
H'0:Finite nat A
x:nat
H'2:~ In nat A x
x0:nat
H'3:Upper_Bound nat nat_po A x0
Included nat (Couple nat x0 x) Integers unfold nat_po; simpl; trivial.X:Ensemble nat
H':Finite nat X
A:Ensemble nat
H'0:Finite nat A
x:nat
H'2:~ In nat A x
x0:nat
H'3:Upper_Bound nat nat_po A x0
H'5:x <= x0
exists m : nat, Upper_Bound nat nat_po (Add nat A x) m
X:Ensemble nat
H':Finite nat X
A:Ensemble nat
H'0:Finite nat A
x:nat
H'2:~ In nat A x
x0:nat
H'3:Upper_Bound nat nat_po A x0
Included nat (Couple nat x0 x) Integers
    exists x0.X:Ensemble nat
H':Finite nat X
A:Ensemble nat
H'0:Finite nat A
x:nat
H'2:~ In nat A x
x0:nat
H'3:Upper_Bound nat nat_po A x0
H'5:x <= x0
Upper_Bound nat nat_po (Add nat A x) x0
X:Ensemble nat
H':Finite nat X
A:Ensemble nat
H'0:Finite nat A
x:nat
H'2:~ In nat A x
x0:nat
H'3:Upper_Bound nat nat_po A x0
Included nat (Couple nat x0 x) Integers
    apply Upper_Bound_definition.X:Ensemble nat
H':Finite nat X
A:Ensemble nat
H'0:Finite nat A
x:nat
H'2:~ In nat A x
x0:nat
H'3:Upper_Bound nat nat_po A x0
H'5:x <= x0
In nat (Carrier_of nat nat_po) x0
X:Ensemble nat
H':Finite nat X
A:Ensemble nat
H'0:Finite nat A
x:nat
H'2:~ In nat A x
x0:nat
H'3:Upper_Bound nat nat_po A x0
H'5:x <= x0
forall y : nat,
In nat (Add nat A x) y -> Rel_of nat nat_po y x0
X:Ensemble nat
H':Finite nat X
A:Ensemble nat
H'0:Finite nat A
x:nat
H'2:~ In nat A x
x0:nat
H'3:Upper_Bound nat nat_po A x0
Included nat (Couple nat x0 x) Integers
      unfold nat_po.X:Ensemble nat
H':Finite nat X
A:Ensemble nat
H'0:Finite nat A
x:nat
H'2:~ In nat A x
x0:nat
H'3:Upper_Bound nat nat_po A x0
H'5:x <= x0
In nat
  (Carrier_of nat
     {|
     Carrier_of := Integers;
     Rel_of := le;
     PO_cond1 := Inhabited_intro nat Integers 0
                   (Integers_defn 0);
     PO_cond2 := le_Order |}) x0
X:Ensemble nat
H':Finite nat X
A:Ensemble nat
H'0:Finite nat A
x:nat
H'2:~ In nat A x
x0:nat
H'3:Upper_Bound nat nat_po A x0
H'5:x <= x0
forall y : nat,
In nat (Add nat A x) y -> Rel_of nat nat_po y x0
X:Ensemble nat
H':Finite nat X
A:Ensemble nat
H'0:Finite nat A
x:nat
H'2:~ In nat A x
x0:nat
H'3:Upper_Bound nat nat_po A x0
Included nat (Couple nat x0 x) Integers simpl.X:Ensemble nat
H':Finite nat X
A:Ensemble nat
H'0:Finite nat A
x:nat
H'2:~ In nat A x
x0:nat
H'3:Upper_Bound nat nat_po A x0
H'5:x <= x0
In nat Integers x0
X:Ensemble nat
H':Finite nat X
A:Ensemble nat
H'0:Finite nat A
x:nat
H'2:~ In nat A x
x0:nat
H'3:Upper_Bound nat nat_po A x0
H'5:x <= x0
forall y : nat,
In nat (Add nat A x) y -> Rel_of nat nat_po y x0
X:Ensemble nat
H':Finite nat X
A:Ensemble nat
H'0:Finite nat A
x:nat
H'2:~ In nat A x
x0:nat
H'3:Upper_Bound nat nat_po A x0
Included nat (Couple nat x0 x) Integers apply triv_nat.X:Ensemble nat
H':Finite nat X
A:Ensemble nat
H'0:Finite nat A
x:nat
H'2:~ In nat A x
x0:nat
H'3:Upper_Bound nat nat_po A x0
H'5:x <= x0
forall y : nat,
In nat (Add nat A x) y -> Rel_of nat nat_po y x0
X:Ensemble nat
H':Finite nat X
A:Ensemble nat
H'0:Finite nat A
x:nat
H'2:~ In nat A x
x0:nat
H'3:Upper_Bound nat nat_po A x0
Included nat (Couple nat x0 x) Integers
    intros y H'1; elim H'1.X:Ensemble nat
H':Finite nat X
A:Ensemble nat
H'0:Finite nat A
x:nat
H'2:~ In nat A x
x0:nat
H'3:Upper_Bound nat nat_po A x0
H'5:x <= x0
y:nat
H'1:In nat (Add nat A x) y
forall x1 : nat,
In nat A x1 -> Rel_of nat nat_po x1 x0
X:Ensemble nat
H':Finite nat X
A:Ensemble nat
H'0:Finite nat A
x:nat
H'2:~ In nat A x
x0:nat
H'3:Upper_Bound nat nat_po A x0
H'5:x <= x0
y:nat
H'1:In nat (Add nat A x) y
forall x1 : nat,
In nat (Singleton nat x) x1 -> Rel_of nat nat_po x1 x0
X:Ensemble nat
H':Finite nat X
A:Ensemble nat
H'0:Finite nat A
x:nat
H'2:~ In nat A x
x0:nat
H'3:Upper_Bound nat nat_po A x0
Included nat (Couple nat x0 x) Integers
    intros x1 H'4; try assumption.X:Ensemble nat
H':Finite nat X
A:Ensemble nat
H'0:Finite nat A
x:nat
H'2:~ In nat A x
x0:nat
H'3:Upper_Bound nat nat_po A x0
H'5:x <= x0
y:nat
H'1:In nat (Add nat A x) y
x1:nat
H'4:In nat A x1
Rel_of nat nat_po x1 x0
X:Ensemble nat
H':Finite nat X
A:Ensemble nat
H'0:Finite nat A
x:nat
H'2:~ In nat A x
x0:nat
H'3:Upper_Bound nat nat_po A x0
H'5:x <= x0
y:nat
H'1:In nat (Add nat A x) y
forall x1 : nat,
In nat (Singleton nat x) x1 -> Rel_of nat nat_po x1 x0
X:Ensemble nat
H':Finite nat X
A:Ensemble nat
H'0:Finite nat A
x:nat
H'2:~ In nat A x
x0:nat
H'3:Upper_Bound nat nat_po A x0
Included nat (Couple nat x0 x) Integers
    elim H'3; simpl; auto with sets arith.X:Ensemble nat
H':Finite nat X
A:Ensemble nat
H'0:Finite nat A
x:nat
H'2:~ In nat A x
x0:nat
H'3:Upper_Bound nat nat_po A x0
H'5:x <= x0
y:nat
H'1:In nat (Add nat A x) y
forall x1 : nat,
In nat (Singleton nat x) x1 -> Rel_of nat nat_po x1 x0
X:Ensemble nat
H':Finite nat X
A:Ensemble nat
H'0:Finite nat A
x:nat
H'2:~ In nat A x
x0:nat
H'3:Upper_Bound nat nat_po A x0
Included nat (Couple nat x0 x) Integers
    intros x1 H'4; elim H'4; auto with sets arith.X:Ensemble nat
H':Finite nat X
A:Ensemble nat
H'0:Finite nat A
x:nat
H'2:~ In nat A x
x0:nat
H'3:Upper_Bound nat nat_po A x0
Included nat (Couple nat x0 x) Integers
    red.X:Ensemble nat
H':Finite nat X
A:Ensemble nat
H'0:Finite nat A
x:nat
H'2:~ In nat A x
x0:nat
H'3:Upper_Bound nat nat_po A x0
forall x1 : nat,
In nat (Couple nat x0 x) x1 -> In nat Integers x1
    intros x1 H'1; elim H'1; apply triv_nat.
  Qed.

  Lemma Integers_has_no_ub :
    ~ (exists m : nat, Upper_Bound nat nat_po Integers m).~ (exists m : nat, Upper_Bound nat nat_po Integers m)
  Proof.~ (exists m : nat, Upper_Bound nat nat_po Integers m)
    red; intro H'; elim H'.H':exists m : nat, Upper_Bound nat nat_po Integers m
forall x : nat,
Upper_Bound nat nat_po Integers x -> False
    intros x H'0.H':exists m : nat, Upper_Bound nat nat_po Integers m
x:nat
H'0:Upper_Bound nat nat_po Integers x
False
    elim H'0; intros H'1 H'2.H':exists m : nat, Upper_Bound nat nat_po Integers m
x:nat
H'0:Upper_Bound nat nat_po Integers x
H'1:In nat (Carrier_of nat nat_po) x
H'2:forall y : nat, In nat Integers y -> Rel_of nat nat_po y x
False
    cut (In nat Integers (S x)).H':exists m : nat, Upper_Bound nat nat_po Integers m
x:nat
H'0:Upper_Bound nat nat_po Integers x
H'1:In nat (Carrier_of nat nat_po) x
H'2:forall y : nat, In nat Integers y -> Rel_of nat nat_po y x
In nat Integers (S x) -> False
H':exists m : nat, Upper_Bound nat nat_po Integers m
x:nat
H'0:Upper_Bound nat nat_po Integers x
H'1:In nat (Carrier_of nat nat_po) x
H'2:forall y : nat, In nat Integers y -> Rel_of nat nat_po y x
In nat Integers (S x)
    intro H'3.H':exists m : nat, Upper_Bound nat nat_po Integers m
x:nat
H'0:Upper_Bound nat nat_po Integers x
H'1:In nat (Carrier_of nat nat_po) x
H'2:forall y : nat, In nat Integers y -> Rel_of nat nat_po y x
H'3:In nat Integers (S x)
False
H':exists m : nat, Upper_Bound nat nat_po Integers m
x:nat
H'0:Upper_Bound nat nat_po Integers x
H'1:In nat (Carrier_of nat nat_po) x
H'2:forall y : nat, In nat Integers y -> Rel_of nat nat_po y x
In nat Integers (S x)
    specialize H'2 with (y := S x); lapply H'2;
      [ intro H'5; clear H'2 | try assumption; clear H'2 ].H':exists m : nat, Upper_Bound nat nat_po Integers m
x:nat
H'0:Upper_Bound nat nat_po Integers x
H'1:In nat (Carrier_of nat nat_po) x
H'3:In nat Integers (S x)
H'5:Rel_of nat nat_po (S x) x
False
H':exists m : nat, Upper_Bound nat nat_po Integers m
x:nat
H'0:Upper_Bound nat nat_po Integers x
H'1:In nat (Carrier_of nat nat_po) x
H'2:forall y : nat, In nat Integers y -> Rel_of nat nat_po y x
In nat Integers (S x)
    simpl in H'5.H':exists m : nat, Upper_Bound nat nat_po Integers m
x:nat
H'0:Upper_Bound nat nat_po Integers x
H'1:In nat (Carrier_of nat nat_po) x
H'3:In nat Integers (S x)
H'5:S x <= x
False
H':exists m : nat, Upper_Bound nat nat_po Integers m
x:nat
H'0:Upper_Bound nat nat_po Integers x
H'1:In nat (Carrier_of nat nat_po) x
H'2:forall y : nat, In nat Integers y -> Rel_of nat nat_po y x
In nat Integers (S x)
    absurd (S x <= x); auto with arith.H':exists m : nat, Upper_Bound nat nat_po Integers m
x:nat
H'0:Upper_Bound nat nat_po Integers x
H'1:In nat (Carrier_of nat nat_po) x
H'2:forall y : nat, In nat Integers y -> Rel_of nat nat_po y x
In nat Integers (S x)
    apply triv_nat.
 Qed.

  Lemma Integers_infinite : ~ Finite nat Integers.~ Finite nat Integers
  Proof.~ Finite nat Integers
    generalize Integers_has_no_ub.~ (exists m : nat, Upper_Bound nat nat_po Integers m) ->
~ Finite nat Integers
    intro H'; red; intro H'0; try exact H'0.H':~
(exists m : nat,
   Upper_Bound nat nat_po Integers m)
H'0:Finite nat Integers
False
    apply H'.H':~
(exists m : nat,
   Upper_Bound nat nat_po Integers m)
H'0:Finite nat Integers
exists m : nat, Upper_Bound nat nat_po Integers m
    apply Finite_subset_has_lub; auto with sets arith.
  Qed.

End Integers_sect.