Library schutte.Schutte

Set Implicit Arguments.

Add LoadPath "../hilbert".
Add LoadPath "../prelude".
Add LoadPath "../denumerable".

Require Import Relations.
Require Import Epsilon.
Require Import Classical.
Require Import Well_Orders.
Require Import Lub.
Require Import Denumerable.
Require Import Compare_dec.
Require Import Coq.Sets.Image.
Require Import PartialFun.
Require Import Classical_sets.
Require Import PartialFix.

Hint Unfold In.
 Implicit Arguments Included [U].

Parameter ON : WO.
Definition OT := M ON.

Definition lt := Lt ON.
Definition le := Le ON.

Notation "a < b" := (lt a b): ord_scope.
Notation "a <= b" := (le a b):ord_scope.

Delimit Scope ord_scope with ord.

Open Scope ord_scope.

Definition ordinal := D ON.

Ltac ordi := match goal with
    [ |- ordinal _ ] => eauto with schutte
 | _ => idtac
end.

Definition Unbounded (X : Ensemble OT) :=
  forall x, ordinal x -> exists y, In X y /\ x < y.

Implicit Arguments denumerable [U].

Axiom AX2 : forall X: Ensemble OT, Included X ordinal ->
                      (exists a, ordinal a /\
                        (forall y, X y -> y < a)) ->
                       denumerable X.

Axiom AX3 : forall X : Ensemble OT,
               denumerable X -> (Included X ordinal) ->
               exists a, ordinal a /\ (forall y, X y -> y < a).

Axiom inh_OT : OT.

Hint Resolve inh_OT : schutte.

Lemma Unbounded_not_denumerable : forall X, Included X ordinal ->
            Unbounded X -> not (denumerable X).
Proof.
 red;intros.
 case (AX3 H1 H).
 intros x (Hx,H'x).
 case (H0 _ Hx).
 intros y (Hy,H'y).
 case (Lt_irreflexive ON x).
 apply (Lt_trans ON x y x).
 auto.
 fold lt;
 auto.
Qed.

Lemma denumerable_not_Unbounded : forall X, Included X ordinal ->
            denumerable X -> not (Unbounded X).
Proof.
 red;intros.
 apply Unbounded_not_denumerable with X;auto.
Qed.

Definition progressive (P : OT -> Prop) : Prop :=
  forall a, ordinal a -> (forall b, ordinal b -> b < a -> P b) -> P a.

Theorem Induction : forall (P: OT->Prop), progressive P ->
                       forall a, ordinal a -> P a.
 Proof.
 intros P Hp.
 case (classic (forall a : OT, ordinal a -> P a));[trivial|idtac].
 intro H.
 case (not_all_ex_not _ (fun a => ordinal a -> P a) H).
 intros x Hx.
 case (imply_to_and _ _ Hx).
 intros Ox P'x.
 elimtype False.
 case (well_order ON (fun z => ~ P z) x Ox P'x).
 intros x0 H0.
 assert (forall b, ordinal b -> b < x0 -> P b).
 intros.
 case H0.
 intros H3 (H4,H5).
 apply NNPP.
 red;intro.
 case (H5 _ H1 H6).
 intro;subst x0.
 case (Lt_irreflexive _ _ H2).
 intro; case (Lt_irreflexive _ b).
 eapply (Lt_trans ON);eauto.
 unfold progressive in Hp.
 assert (~ (P x0)).
 case H0.
 unfold In;
 tauto.
 apply H2.
 apply Hp.
 case H0;tauto.
 auto.
Qed.

Lemma le_refl : forall alpha, ordinal alpha -> alpha <= alpha.
Proof.
 left;auto.
Qed.

Hint Resolve le_refl : schutte.

Lemma eq_le : forall a b, ordinal a -> a = b -> a <= b.
left;auto.
Qed.

Lemma lt_le : forall a b, a < b -> a <= b.
 right;auto.
Qed.

Lemma lt_trans : forall a b c, a < b -> b < c -> a < c.
Proof (Lt_trans ON).

Lemma le_lt_trans : forall a b c, a <= b -> b < c -> a < c.
Proof (Le_Lt_trans (Wo:=ON)).

Lemma lt_le_trans : forall a b c, a < b -> b <= c -> a < c.
Proof (Lt_Le_trans (Wo:=ON)).

Lemma le_trans : forall a b c, a <= b -> b <= c -> a <= c.
Proof (Le_trans (Wo := ON)).

Lemma lt_irr : forall a, ~ (a < a).
Proof (Lt_irreflexive ON).

Lemma le_antisym : forall a b, a <= b -> b <= a -> a = b.
Proof (Le_antisym (Wo:=ON)).

Lemma le_eq_or_lt : forall a b, a <= b -> a = b \/ a < b.
Proof.
  intros a b [(_,H)|H];auto.
Qed.

Lemma le_not_gt : forall a b, a <= b -> ~ b < a.
Proof.
 intros a b H; case (le_eq_or_lt H).
 intro;subst b;apply lt_irr.
 intros H0 H1;case (lt_irr a);eapply lt_trans;eauto.
Qed.

Hint Resolve eq_le lt_le lt_trans le_trans le_lt_trans
   lt_le_trans lt_irr le_not_gt:
  schutte.

Lemma lt_ordinal : forall a b, a < b -> ordinal a.
Proof.
 intros; unfold ordinal.
 generalize (Lt_inc_D1 ON a);auto.

 intro.
 eapply H0.
 eauto.
Qed.

Lemma gt_ordinal : forall a b, a < b -> ordinal b.
Proof.
 intros; generalize (Lt_inc_D2 ON a); unfold In.
 intro H0;eapply H0.
 auto.
Qed.

Lemma le_ordinal : forall a b, a <= b -> ordinal a.
Proof.
 destruct 1.
 case H;auto.
 eapply lt_ordinal; eauto.
Qed.

Lemma ge_ordinal : forall a b, a <= b -> ordinal b.
Proof.
 destruct 1.
 case H;intros;subst b;auto.
  eapply gt_ordinal; eauto.
Qed.

Lemma le_disj : forall alpha beta, alpha <= beta -> alpha = beta \/ alpha < beta.
Proof.
  intros.
  elim H;auto.
   destruct 1;auto.
Qed.

Hint Resolve lt_ordinal gt_ordinal le_ordinal ge_ordinal : schutte.

Lemma all_ord_acc : forall alpha, ordinal alpha -> Acc lt alpha.
 intros.
 pattern alpha.
 apply Induction.
 red.
 intros.
 split.
 intros.
 apply H1.
 ordi.
 auto.
 auto.
Qed.

Lemma trichotomy : forall a b, ordinal a -> ordinal b ->
                           a < b \/ a = b \/ b < a.
Proof (Lt_connect ON).

Ltac tricho t u Hname := case (trichotomy t u);
                           [auto with schutte |
                            auto with schutte |
                            intro Hname |
                            intros [Hname|Hname]].

Lemma lt_or_ge : forall a b, ordinal a -> ordinal b -> a < b \/ b <= a.
Proof.
 intros a b Ha Hb; tricho a b H;auto with schutte.
Qed.

Lemma not_gt_le : forall a b, ordinal a -> ordinal b -> ~(b<a) -> a <= b.
 intros.
 tricho a b H2; auto with schutte.
 case (H1 H2).
Qed.

Hint Unfold Included.
Theorem Non_denum : ~ denumerable ordinal.
Proof.
 red; intro H.
 case (AX3 H).
 auto.
 intros x (H1,H2).
 case (lt_irr x);auto.
Qed.

Definition zero_spec (z:OT) := ordinal z /\
                                 forall a, ordinal a -> z <= a.

Definition zero : OT.
 the_i zero_spec.
 auto with schutte.
 case (AX3 (X:=Empty_set _)).
 apply denumerable_empty.
 unfold Included; contradiction.
 intros x (Hx,H'x).
 case (well_order ON ordinal x);auto.
 intros z (H1,(_,H2)).
 exists z;unfold zero_spec.
 repeat split;auto.
 intros x1 D1.
 generalize (H2 _ D1 D1).
 fold lt.
 destruct 1; auto with schutte.
 intros y (Hy,H'y).
 apply le_antisym;auto.
 case (H2 y);auto with schutte.
Defined.

Theorem ordinal_zero : ordinal zero.
Proof.
 hilbert_e.
 destruct 1;auto.
Qed.

Hint Resolve ordinal_zero : schutte.

Lemma le_zero : forall a, ordinal a -> zero <= a.
Proof.
 intros;pattern zero; hilbert_e.
 unfold zero_spec ;intuition.
Qed.


Lemma not_lt_zero_0 : forall a, ordinal a -> ~ a < zero.
Proof.
 intros;apply le_not_gt.
 apply le_zero;auto.
Qed.

Lemma not_lt_zero : forall a, ~ a < zero.
Proof.
  red; intros.
  case (not_lt_zero_0 a (lt_ordinal _ _ H) H).
Qed.


Lemma zero_or_greater : forall a, ordinal a ->
                 a = zero \/ exists b, ordinal b /\ b < a.
Proof.
 intros a Ha.
 tricho zero a t;auto with schutte.
 right;exists zero;auto with schutte.
 case (not_lt_zero a t).
Qed.

Lemma zero_or_positive : forall a, ordinal a ->
                 a = zero \/ zero < a.
Proof.
 intros a Ha.
 tricho zero a t;auto with schutte.
 case (not_lt_zero a t).
Qed.

Theorem unbounded : forall alpha, ordinal alpha -> exists beta, ordinal beta /\
                                                             alpha < beta.
Proof.
 intros.
 pose (X0 := fun z => z < alpha /\ ordinal z).
 assert (denumerable X0).
 apply AX2.
 unfold X0, Included, In.
 intuition.
 exists alpha.
 split;auto.
 unfold X0;intuition.
 pose (X:= Add _ X0 alpha).
 assert (denumerable X).
 unfold X; unfold Add; apply denumerable_union.
 auto.
 apply denumerable_singleton.
 case (AX3 H1).
 unfold X; intros x Hx.
 case Hx.
 2:inversion 1.
 2: subst x0; unfold In;auto.
 unfold In, X0;tauto.
 intros beta (Hb,H'b).
 exists beta.
 split;auto.
 apply H'b.
 unfold X;auto.
 right;split.
Qed.

Definition the_least : (OT -> Prop) -> OT.
 the_fun_i ( fun (X:OT -> Prop) => Inhabited _ X
                  /\ Included X ordinal)
       (fun X l => (is_least_member (ordinal) lt X l)).

 exact inh_OT.

 destruct 1.
 case H.

 intros.

 generalize (well_order ON a x (H0 _ H1) H1);auto.
 destruct 1;intros.
 exists x0;repeat split; auto.
 case H2;auto.
 case H2;auto.
 tauto.
 case H2;auto.
 tauto.


 intros; eapply least_member_unicity;eauto.

Defined.

Lemma the_least_ordinal : the_least ordinal = zero.
Proof.
 pattern ordinal, (the_least ordinal).
 pfun_e.

 split;auto with schutte.
 exists zero;auto with schutte.
 intros b (H,_) H0.
 case H0.
 intros H1 (_,H2).
 case (H2 _ ordinal_zero).
 exact ordinal_zero.
 auto.
 intro H3; case (not_lt_zero _ H3).
Qed.

Lemma the_least_ok : forall X, Inhabited OT X -> Included X ordinal ->
    forall a, X a -> the_least X <= a.
Proof.
 intros.
 pattern X, (the_least X).
 pfun_e.
 unfold le.
 unfold is_least_member;auto.
 red.
 intros.
 decompose [and] H3.
 case (H7 a (H0 a H1) H1);auto.
Qed.

Definition succ_spec (a:OT) := is_least_member (ordinal) lt (fun z => a < z).

Definition succ : OT -> OT.
 the_fun_i ordinal succ_spec.
 exact inh_OT.
 intros.
 case (unbounded a H).
 intros x (Ox, Hx).
 case (well_order ON (fun z => lt a z) x Ox Hx);auto.
 intros s Hs;exists s.
 split;auto.
 unfold succ_spec;intros.
eapply least_member_unicity; eauto.
Defined.

Definition is_succ (a:OT) := exists b, ordinal b /\ a = succ b.

Lemma lt_succ : forall a, ordinal a -> a < succ a.
Proof.
 intros; pattern a,(succ a).
 pfun_e.
 destruct 2;tauto.
Qed.

Hint Resolve lt_succ : schutte.

Lemma ordinal_succ : forall a , ordinal a -> ordinal (succ a).
Proof.
 intros a H.
 pattern a, (succ a).
 pfun_e.
 destruct 2;auto.
Qed.

Hint Resolve ordinal_succ : schutte.

Lemma succ_rw : forall a, ordinal a -> succ a = the_least
                                                  (fun x => a < x).
Proof.
 intros.
 pattern a, (succ a).
 pfun_e.
 intros.
 pattern (fun x : OT => a < x),(the_least (fun x : OT => a < x)).
 pfun_e.
 split.
 exists (succ a).
 red.
 auto with schutte.
 eauto with schutte.
 intros.
 generalize ( least_member_unicity ON (X:=fun x : OT => a < x) (a:=b1)(b:=b0) H3).
 intro H4;symmetry;apply H4.
 exact H1.
Qed.

Lemma lt_succ_le : forall a b,
    a < b -> succ a <= b.
Proof.
 intros a b H; pattern a,(succ a).
 pfun_e.
 ordi.
 intros.
 red in H1.
 red in H1; decompose [and] H1.
 case (H5 b ).
 red;ordi.
 auto.
 auto with schutte.
 auto with schutte.
Qed.

Lemma lt_succ_le_2 : forall a b,
                       ordinal b ->
                       a < succ b ->
                       a <= b.
Proof.
 intros.
  tricho a b t;eauto with schutte.
   case (lt_irr a).
 apply lt_le_trans with (succ b).
 assumption.
 apply lt_succ_le;eauto with schutte.
Qed.

Lemma succ_mono : forall a b, ordinal a -> ordinal b ->
          a < b -> succ a < succ b.
Proof.
 intros.
 eapply le_lt_trans.
 eapply lt_succ_le;eauto.
 auto with schutte.
Qed.

Implicit Arguments succ_mono [ a b].

Lemma succ_monoR : forall a b, ordinal a -> ordinal b ->
        succ a < succ b -> a < b.
Proof.
 intros.
 tricho a b t; auto with schutte.
 subst b; case (lt_irr (succ a)); eauto with schutte.
 case (lt_irr (succ a)).
 eapply lt_trans;eauto.
 apply succ_mono;auto.
Qed.

Lemma succ_injection : forall a b, ordinal a -> ordinal b ->
                                   succ a = succ b -> a=b.
Proof.
 intros.
 tricho a b t;auto.
 generalize (succ_mono H H0 t).
 rewrite H1; intro; case (lt_irr (succ b));auto.
 generalize (succ_mono H0 H t).
 rewrite H1; intro; case (lt_irr (succ b));auto.
Qed.

Lemma succ_zero_diff : forall a , ordinal a -> succ a <> zero.
Proof.
 intros; pattern a,(succ a).
 pfun_e.
 unfold succ_spec.
 red;intros.
 subst b0.
 case H1.
 intros.
 case H3.
 intros.
 red in H4.
 case (not_lt_zero _ H4).
Qed.

Lemma zero_lt_succ : forall alpha, ordinal alpha -> zero < succ alpha.
Proof.
   intros a Ha; apply le_lt_trans with a;eauto with schutte.
   apply le_zero;auto.
Qed.

  Hint Resolve zero_lt_succ le_zero : schutte.

Reserved Notation "'F' n" (at level 29) .
Fixpoint finite (i:nat) : OT :=
  match i with 0 => zero
             | S i=> succ (F i)
  end
where "'F' i" := (finite i) : ord_scope.

Lemma ordinal_finite : forall i, ordinal (F i).
Proof.
 induction i; simpl; auto with schutte.
Qed.

Hint Resolve ordinal_finite : schutte.

Lemma finite_lt_inv : forall i o, o < F i ->
                       exists j:nat , (j<i)%nat /\ o= F j.
Proof.
 induction i.
 simpl (F 0).
 intros.
 case (not_lt_zero _ H ).
 simpl (F (S i));intros.
 case (lt_succ_le_2 o (F i));auto with schutte.
 exists i.
 case H0;intros;
 subst o;auto with arith.
 intro.
 case (IHi o H0).
 intros.
 exists x; case H1;auto with arith.
Qed.

Lemma finite_mono : forall i j, (i<j)%nat -> F i < F j.
Proof.
 induction 1.
 simpl (finite (S i)).
 auto with schutte.
 apply lt_trans with (finite m);auto.
 simpl (finite (S m)).
 apply lt_succ; auto with schutte.
Qed.

Hint Resolve finite_mono : schutte.

Lemma finite_inj : forall i j, F i = F j -> i = j.
Proof.
 intros.
 case (lt_eq_lt_dec i j).
 destruct 1.
 case (lt_irr (F i)).
 pattern (F i) at 2 ; rewrite H.
 apply finite_mono;auto.
 auto.
 intro; case (lt_irr (F i)).
 pattern (F i) at 1 ; rewrite H.
 apply finite_mono;auto.
Qed.

Definition is_finite := seq_range finite.

Definition sup_spec X l := is_lub (ordinal) lt X l.

Lemma sup_exists : forall X, denumerable X ->
                             Included X ordinal ->
                             ex (sup_spec X).
Proof.
 unfold Included, In.
 intros X H H0.
 case (AX3 H).
 auto.
 intros x (Hx,H'x).
 assert (H''x : forall y : OT, X y -> y=x \/ lt y x).
 intuition.
 generalize (well_order ON
                          (fun z => ordinal z /\
                            (forall y, ordinal y -> X y -> y=z \/ y < z))
                          x Hx ).
 intros.
 case H1;intros.
 auto.
 exists x0.
 unfold is_least_member in H2.
 repeat split.
 case H2.
 auto.
 case H2.
 intros.
 intuition.
 red.
 intros.
 case H2.
 intros.
 apply H11;auto.
 intros.
 decompose [and] H2.

 apply H8.
 assumption.
 split.
 assumption.
 intuition.
Qed.

Lemma sup_unicity : forall X l l',
    (denumerable X /\
                             forall x, X x -> ordinal x) ->
    sup_spec X l -> sup_spec X l' -> l = l'.
Proof.
 intros X l l' _ H H0.
 apply le_antisym.
 case H.
 case H0.
 intuition.
 case (H7 l' H1);auto with schutte.
 case H;case H0;intuition.
 case (H6 l H3);auto with schutte.
Qed.

Definition sup (X:OT->Prop) : OT.
 the_fun_i ( fun (X:OT -> Prop) => denumerable X /\ Included X ordinal )
           sup_spec.

 auto with schutte.
 exact inh_OT.
  intro X;destruct 1 as [H1 H2]; ex_unic_intro;auto.

 apply sup_exists;auto.
 intros;apply sup_unicity with X;auto.
Defined.

Notation "'|_|' X" := (sup X) (at level 29) : ord_scope.

Definition is_limit (a:OT) := ordinal a /\ a <> zero /\ ~ (is_succ a).

Lemma lt_succ_lt : forall a b, is_limit b ->
                   a < b -> succ a < b.
Proof.
 intros a b (Ob,(Zb,Sb)) H .
 case (lt_succ_le a b H).
 intros (_,H') ; subst b.
 case Sb.
 exists a;eauto with schutte.
 auto.
Qed.

Lemma sup_upper_bound : forall (X: OT -> Prop) x, denumerable X ->
                  (forall x, X x -> ordinal x) -> X x -> x <= |_| X.
Proof.
 intros X x H H0.
 pattern X,(sup X).
 pfun_e.
 unfold sup_spec;intros.
 intuition.
 case H2.
 intuition.

 case (H7 x); auto with schutte.
Qed.


Lemma sup_least_upper_bound : forall (X: OT->Prop) x, denumerable X ->
                   (forall y, X y -> ordinal y) -> ordinal x ->
                   (forall y, X y -> y <= x) -> |_| X <= x.
Proof.
 intros.
 pattern X, (sup X).
 pfun_e.
 intros .
 clear H3.
 red in H4.
 red in H4; decompose [and] H4.
 unfold upper_bound in H6.
 case (H7 _ H1);auto with schutte.
 intros.
 unfold upper_bound;intros.
 case (H2 _ H8);auto.
 destruct 1;auto.
Qed.

Lemma sup_ordinal : forall X, denumerable X ->
                              (forall x, X x -> ordinal x) ->
                              ordinal (|_| X).
Proof.
 intros X HX H.
 pattern X, (|_| X).
 pfun_e.
 unfold sup_spec;intuition.
 case H1;auto.
Qed.

Hint Resolve sup_ordinal : schutte.

Lemma sup_of_leq : forall a, ordinal a -> a = |_| (fun x => ordinal x /\
                                                            x <= a).
Proof.
 intros;pattern (fun x => ordinal x /\ x<=a),(|_| (fun x => ordinal x /\ x <= a)).
 pfun_e.
 intuition.
 assert (denumerable (fun x : OT => ordinal x /\ x <= a)).
 apply AX2.
 unfold Included, In, ordinal;tauto.
 exists (succ a).
 split; auto with schutte.
 destruct 1.
 apply le_lt_trans with a;eauto with schutte.
 auto.
 intros.
 red;intros.
 case H0.
 auto.
 destruct 1.
 destruct 1.
 decompose [and] H3.
 case (H5 a H).
 unfold upper_bound.
 intros; apply le_eq_or_lt;auto.
 case H7;auto.
 auto.

 intro.
 case (lt_irr a).
 apply le_lt_trans with b0;eauto with schutte.
 case (H4 a);unfold In;auto with schutte.
Qed.

Lemma sup_mono : forall (X Y : Ensemble OT),
                 denumerable X ->
                 denumerable Y ->
                 (Included X ordinal) ->
                 (Included Y ordinal) ->
                 (forall x, In X x -> exists y, In Y y /\ x <= y) ->
                 |_| X <= |_| Y.
Proof.
 intros.
 apply sup_least_upper_bound; auto with schutte.
 intros x Hx; case (H3 x Hx); intros y (Hy,Hy').
 apply le_trans with y;auto with schutte.
 apply sup_upper_bound;auto with schutte.
Qed.

Lemma sup_eq_intro : forall (X Y : Ensemble OT),
                 denumerable X ->
                 denumerable Y ->
                 (Included X ordinal) ->
                 (Included Y ordinal) ->
                 (Included X Y) ->
                 (Included Y X) ->
                 |_| X = |_| Y.
Proof.
  unfold Included, In; intros; apply le_antisym; apply sup_mono;auto with schutte;
   intro x;exists x; unfold In;auto with schutte.
Qed.

Lemma lt_sup_exists_leq : forall X, denumerable X ->
                          (Included X ordinal) ->
                          forall y, ordinal y -> y < sup X ->
                          exists x, In X x /\ y <= x.
Proof.
 intros.
 case (not_all_not_ex _ (fun x => X x /\ y <= x)).
 2 : intros x Hx; exists x;auto.
 red;intro.
 unfold Included, In , ordinal in H0.

 assert (forall n, X n -> n < y).
 intro.
 intro.
 apply NNPP.
 red;intro.
 assert (y < n).
 case (trichotomy n y).

 apply H0;auto.
 auto.
 intro; case H5;auto.
 destruct 1.
 subst n.
  case (H3 y).
 auto with schutte.
 auto.
 case (H3 n).
 split;auto with schutte.
 clear H3.
  case (lt_irr y).
 eapply lt_le_trans with (|_|X);eauto.
 apply sup_least_upper_bound;auto with schutte.
Qed.

Lemma lt_sup_exists_lt : forall X, denumerable X ->
                          Included X ordinal ->
                          forall y, ordinal y -> y < sup X ->
                          exists x, In X x /\ y < x.
Proof.

 intros.
 unfold Included, In in H0.
  case (not_all_not_ex _ (fun x => X x /\ y < x)).
 2 : intros x Hx; exists x;auto.
 red;intro.
 assert (forall n, X n -> n <= y).
 intro.
 intro.
 apply NNPP.
 red;intro.
 assert (y < n).
 case (trichotomy n y).
 apply H0;auto.
 auto.
 intro.
 case H5;auto with schutte.
  destruct 1.
 case H5;auto with schutte.
 auto.
 case (H3 n).
 split;auto with schutte.
 assert (sup X <= y).
 apply sup_least_upper_bound.
 auto.
 auto.
 auto.
 auto.
 case (Lt_irreflexive ON y).
 eapply Lt_Le_trans;eauto.
Qed.

Definition members (a:OT) := Intersection _ ordinal (fun b => b < a).

Lemma members_eq : forall a b, ordinal a -> ordinal b ->
                               members a = members b -> a = b.
Proof.
  intros.
  tricho a b H2.
 assert (members b a).
 split;auto.
 assert (~(members a a)).
 red; inversion_clear 1.
 case (lt_irr a);auto.
 rewrite H1 in H4.
 case H4;auto.
 auto.
  assert (members a b).
 split;auto.
 assert (~(members b b)).
 red;inversion_clear 1.
 case (lt_irr b);auto.
 rewrite <- H1 in H4.
 case H4;auto.
Qed.


Lemma sup_members_succ : forall a, ordinal a ->
                    (sup (members a)) < a ->
                    a = succ (|_| (members a)).
Proof.
 intros a H;pose (A := sup (members a)).
 fold A.
 generalize (lt_succ_le A a).
 intros.
 assert (ordinal A).
 unfold A;apply sup_ordinal.
 apply AX2.
 unfold Included, In, members. destruct 1;tauto.
 exists a;unfold members.
 split;auto;destruct 1.
 auto.
 unfold members.
 destruct 1.
 auto.
 case (le_eq_or_lt (H0 H1)).
 symmetry;auto.
 intro H3.
 assert (succ A <= A).
 unfold A;apply sup_upper_bound.
 apply AX2.
 unfold Included. destruct 1; auto.
 exists a;unfold members.
 split; auto.
 destruct 1;auto.
 unfold members;destruct 1;auto.
 unfold members at 1.
 split.
 fold A.
 unfold In; apply ordinal_succ.
 auto.
 unfold In.
  auto.
 case (lt_irr A).
 eapply lt_le_trans.
 eapply lt_succ;eauto.
 auto.
Qed.

Lemma sup_members_not_succ : forall a b, ordinal a -> ordinal b ->
            a = sup (members a) -> a <> succ b.
Proof.
 intros a b Ha Hb e e1.
 generalize (sup_of_leq b Hb).
 intro.
 assert (sup (members a) = b).
 unfold members;rewrite H.
 apply sup_eq_intro.
 apply AX2.
 auto.
 apply Intersection_decreases_l.
exists a. split;auto.
 destruct 1.
 auto.
 apply AX2.
 unfold Included. destruct 1.
 auto.
 exists (succ b).
 split;auto with schutte.
 intros y (Hy,H'y).
 eauto with schutte.
 apply Intersection_decreases_l.
unfold Included. destruct 1.
 auto.
 unfold Included. destruct 1.
 split; auto.
 unfold In in H1.
 rewrite e1 in H1.
 apply lt_succ_le_2;auto.
 unfold Included, In.
 intros x (H1,H2).
 split;auto with schutte.
 unfold In.


 rewrite e1.
 eapply le_lt_trans;eauto with schutte.
 case (lt_irr a).
 pattern a at 2;rewrite e1.
 rewrite e;rewrite H0.
 auto with schutte.
Qed.

Definition omega_limit (f:nat->OT) : OT
                                   := |_| (seq_range f).

Definition seq_mono (f:nat -> OT) :=
   forall i j, (i<j)%nat -> f i < f j.

Lemma seq_mono_intro : forall f,
              (forall i, f i < f (S i)) -> seq_mono f.
Proof.
 intros f H; unfold seq_mono; induction 1.
 auto.
 apply (Lt_trans ON) with (f m);auto.
 apply H.
Qed.

Lemma seq_mono_inj : forall f,
              seq_mono f -> injective _ _ f.
Proof.
 unfold injective;intros f H i j H0.
 case (lt_eq_lt_dec i j).
 destruct 1.
 generalize (H _ _ l).
 rewrite H0;intro;case (Lt_irreflexive ON ( f j));auto.
 auto.
 intro l;generalize (H _ _ l).
 rewrite H0;intro;case (Lt_irreflexive ON ( f j));auto.
Qed.


Lemma seq_range_denumerable : forall f,
  seq_mono f -> denumerable (seq_range f).
Proof.
intros f _.
apply Denumerable.seq_range_denumerable.
Qed.

Hint Resolve seq_range_denumerable seq_mono_intro : schutte.

Lemma lt_omega_limit : forall f , (forall i, ordinal (f i)) ->
                                  seq_mono f ->
                                  forall i, f i < omega_limit f.
Proof.
 unfold omega_limit;intros.
  apply lt_le_trans with (f (S i)).
 eapply H0.
 auto.
 apply sup_upper_bound;auto with schutte.
 destruct 1.
 subst x;auto.
 exists (S i);auto.
Qed.

Definition omega := omega_limit finite.

Lemma finite_lt_omega : forall i, F i < omega.
Proof.
 unfold omega ; intros.
 apply lt_omega_limit; auto with schutte.
Qed.

Lemma lt_omega_finite : forall a, a < omega ->
                                             exists i:nat, a = F i.
Proof.
 unfold omega;intros a H0.
 assert (H:ordinal a).
 eauto with schutte.
 unfold omega_limit in H0.
 generalize (lt_sup_exists_leq (X:=(seq_range finite)) ).
 intros.
 assert (denumerable (seq_range finite)).
 apply seq_range_denumerable.
 unfold seq_mono;intros;apply finite_mono;auto.
 generalize (H1 H2);clear H1;intros.
 assert (forall y : OT, seq_range finite y -> ordinal y).
 destruct 1.
 subst y;auto with schutte.
  generalize (H1 H3);clear H1;intros.
 case (H1 a H H0).
 destruct 1.
 case H5.
 intros (_,H6);subst a.
 case H4.
 intros.
 exists x0;auto.
 case H4;intros.
 subst x.
 case (finite_lt_inv x0 a);auto.
 intros x (H8,H9);exists x;auto.
Qed.

Lemma ordinal_omega_limit : forall s, (forall i, s i < s (S i)) ->
                                       ordinal (omega_limit s).
Proof.
 unfold omega_limit.
 intros;apply sup_ordinal.
  apply seq_range_denumerable;auto.
  red; apply seq_mono_intro; auto.
 destruct 1.
 subst x;auto with schutte.
 eauto with schutte.
Qed.

Lemma ordinal_omega : ordinal omega.
 unfold omega; apply ordinal_omega_limit.
 auto with schutte arith.
Qed.

Lemma lt_omega_limit_lt_exists_lt : forall alpha s,
                                             (forall i, s i < s (S i)) ->
                                              alpha < omega_limit s ->
                                              exists j, alpha < s j.
Proof.
 intros.
 unfold omega_limit in H0.
 assert (exists y, In (seq_range s) y /\ alpha < y).
 apply lt_sup_exists_lt; auto with schutte.
 red;red;red.
 destruct 1;auto.
 subst x;eauto with schutte.
 fold ordinal;eauto with schutte.
 eauto with schutte.
 case H1; intros y Hy.
 case Hy;destruct 1.
 subst y;exists x;auto.
Qed.

 Hint Resolve ordinal_omega ordinal_omega_limit : schutte.
Lemma is_limit_omega : is_limit omega.

Proof.
 unfold is_limit.
 repeat split; auto with schutte.
 red;intro.
 absurd (F 1 < zero).
apply not_lt_zero;auto with schutte.
 rewrite <- H.
 apply finite_lt_omega.
 red;intro.
 case H.
 intros x (Ox,Ex).
 assert (x < omega).
 rewrite Ex;auto with schutte.
 case (lt_omega_finite _ H0).
 intros; subst x.
 assert (omega = F (S x0)).
 simpl;auto.
 case (lt_irr omega);auto with schutte.
 pattern omega at 1;rewrite H1;auto with schutte.
 apply finite_lt_omega;auto with schutte.
Qed.

Lemma not_is_succ_zero : ~ (is_succ zero).
Proof.
  red. intros (b, (Hb,Hb')).
 case (succ_zero_diff _ Hb).
 auto.
Qed.

Lemma not_is_limit_zero : ~ (is_limit zero).
Proof.
 unfold is_limit.
 tauto.
Qed.

Lemma not_is_limit_succ : forall a, ordinal a -> is_succ a -> ~ (is_limit a).
Proof.
 unfold is_limit;tauto.
Qed.

Lemma not_is_succ_limit : forall a, ordinal a -> is_limit a -> ~(is_succ a).
Proof.
 unfold is_limit;tauto.
Qed.

Lemma is_limit_ordinal : forall a, is_limit a -> ordinal a.
Proof.
 unfold is_limit;tauto.
Qed.

Lemma is_succ_ordinal : forall a, is_succ a -> ordinal a.
Proof.
 unfold is_succ.
 intros a (b,(Hb,H'b)).
 subst a; auto with schutte.
Qed.

Hint Resolve is_limit_ordinal is_succ_ordinal : schutte.

Lemma denumerable_members : forall a, ordinal a -> denumerable (members a).
Proof.
 intros a Ha.
 apply AX2.
 unfold members.
 apply Intersection_decreases_l.
 exists a; split ; auto.
   destruct 1. auto.
Qed.

Hint Resolve denumerable_members : schutte.

Lemma le_sup_members : forall a, ordinal a -> |_| (members a) <= a.
Proof.
 intros; apply sup_least_upper_bound; auto with schutte.
 destruct 1; auto.
 destruct 1;auto.
 right; auto.
Qed.

Lemma is_limit_sup_members : forall a, is_limit a -> a = |_| (members a).
Proof.
 intros.
 case (le_sup_members a);auto with schutte.
 intuition.

 intro; generalize (sup_members_succ a).

 intuition.

 generalize (H1 (is_limit_ordinal H) H0).
 intro.
 case (not_is_limit_succ (a:=a));auto with schutte.
 exists (|_|members a).
 split;auto.
 apply sup_ordinal;auto with schutte.
 destruct 1;auto.
Qed.

Lemma sup_members_disj : forall a, ordinal a -> a = sup (members a) ->
                                   a = zero \/ is_limit a.
Proof.
 intros.
 unfold is_limit.
 case (classic (a=zero)).
 auto.
 right;repeat split;auto.
 red;intro H2.
 case H2;intros x (H3,H4).
 case (sup_members_not_succ _ H H3 H0).
 auto.
Qed.

Lemma ordinal_sup_members : forall a, ordinal a ->
                                      ordinal (sup (members a)).
Proof.
 intros; apply sup_ordinal; auto with schutte.
 destruct 1;auto.
Qed.

Theorem classification : forall a, ordinal a -> a = zero \/
                                                is_succ a \/
                                                is_limit a.
Proof.
 intros a Ha.
 case (le_sup_members a Ha).
 intro;case (sup_members_disj Ha);auto with schutte.
 case H;auto.
 right.
 left.
 exists (sup (members a)).
 split.
 apply ordinal_sup_members;auto.
 apply sup_members_succ;auto.
Qed.

Definition set_eq (X Y: OT -> Prop) := forall a, ordinal a -> (X a <-> Y a).

Implicit Arguments Same_set [U].


Lemma members_omega : Same_set (members omega) is_finite.
Proof.
 unfold Same_set;split.
 red. unfold members, In.

destruct 1.

 case (lt_omega_finite x H0).
 intros;exists x0;auto.
 unfold Included, members.

 destruct 1.
 subst x;split;red;auto with schutte.
 apply finite_lt_omega.
Qed.

Inductive closed (B : Ensemble OT) : Prop :=
closed_intro : Included B ordinal ->
               (forall M, Included M B -> Inhabited _ M -> denumerable M -> In B (sup M )) ->
               closed B.

Inductive continuous (f:OT->OT)(A B : Ensemble OT) : Prop :=
  continuous_intro : fun_codomain A B f ->
                     closed A ->
                     (forall U, Included U A -> Inhabited _ U ->
                        denumerable U -> sup (image U f) = f (sup U)) ->
                     continuous f A B.

Lemma Not_Unbounded_bounded : forall X, Included X ordinal ->
              not (Unbounded X) ->
              exists beta, ordinal beta /\ forall x, In X x -> x < beta.
Proof.
 intros.
 apply NNPP.
 red;intro.
 assert (forall beta, ordinal beta ->
                          exists x, In X x /\ beta <= x).
 Focus 2.
 clear H1.
 case H0.
 red;intro.
 intros.
 case (H2 (succ x)).
 auto with schutte.
 intros.
 exists x0;split;auto with schutte.
 case H3;auto.
 case H3;intros.
 apply lt_le_trans with (succ x).
 auto with schutte.

 auto.

intro.
 intros.
 change (exists x:OT, (fun y => In X y /\ beta <= y) x).
 apply not_all_not_ex.
 red;intro.
 case H1.
 exists beta; split;auto.
 intros.
 tricho x beta H5;auto with schutte.
 apply H;auto.

 case (H3 x).
 split;auto with schutte.
 case (H3 x);split;auto with schutte.
Qed.


Lemma Not_Unbounded_denumerable : forall X, Included X ordinal ->
          not (Unbounded X) -> denumerable X.
 intros;eapply AX2;eauto.
 case (Not_Unbounded_bounded H);auto.
 intros.
 exists x;auto.
Qed.

Lemma not_denumerable_unbounded : forall X, Included X ordinal ->
                                   not (denumerable X) -> Unbounded X.
Proof.
 intros.
 apply NNPP.
 red;intro.
 apply H0;apply Not_Unbounded_denumerable;auto.
Qed.

Lemma le_alpha_zero : forall alpha, alpha <= zero -> alpha = zero.
Proof.
 intros.
 apply le_antisym;auto.
 apply le_zero.
 eauto with schutte.
Qed.