Library schutte.Ordering_Functions


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

Require Import Epsilon.
Require Import Schutte.
Require Import Ensembles.
Require Import Well_Orders.
Require Import Denumerable.
Require Import PartialFun.
Require Import Classical.

Set Implicit Arguments.

 Lemma inh_Ordinal_sets : Ensemble OT.
 Proof.
  exact (fun (o:OT) => False); auto.
 Qed.

 Lemma inh_OT_OT : (OT -> OT).
  exact (fun (alpha:OT) => alpha).
 Qed.

Hint Resolve inh_OT_OT inh_Ordinal_sets : schutte.

Definition O_segment (A: Ensemble OT) :=
  Included A ordinal /\
  forall a b, A a -> b < a -> A b.

Definition proper_O_segment (A:OT->Prop) := O_segment A /\
                                          ~ (Same_set A ordinal).

Lemma ordinal_O_segment : O_segment ordinal.
Proof.
 split;auto.
 eauto with schutte.
Qed.

Lemma members_proper : forall a, ordinal a ->
  proper_O_segment (members a).
Proof.
 split.
 split.
 red; destruct 1;auto.
 destruct 1.
 split;auto.
 unfold In.
 eauto with schutte.
 red.
 eauto with schutte.
 unfold Same_set.
 red;destruct 1.
 absurd (succ a < a).
 intro;
 case (le_not_gt (a:=a) (b:=succ a)); auto with schutte.
 case (H1 (succ a)).
 unfold In;auto with schutte.
 auto.
Qed.

Lemma proper_members : forall A, proper_O_segment A -> exists a,
                                        ordinal a /\
                                        Same_set A (members a).
destruct 1.
 unfold O_segment in H.
 case (not_all_not_ex _ (fun b => ordinal b /\ ~ A b)).
 red; intro.
 unfold Same_set in H0.
 apply H0;split.
 unfold Included; case H;auto.
 red; intros.
 unfold In.
 apply NNPP.
 red; intro.
 apply (H1 x).
 split;auto.
 intros.
 case (well_order ON (fun x => ordinal x /\ ~ A x) x).
 case H1;auto.
 auto.
 intros y Hy.
 case Hy;intros H2 ((H3,H4),H5).
 exists y;split.
 auto.
 red; unfold In; split. intros a H6.
 tricho a y T.
 case H;auto.
 intros.
 apply H7;auto.
 split;auto.
 unfold In.
 case H;auto.
 intros.
 apply H7;auto.
 subst y.
 case H4;auto.
 case H4.
 case H;intros.
 apply (H8 a);auto.
 red; unfold In;intros.
 apply NNPP.
 case Hy.
 intros _ ((H7,H8),H9).
 red; intro H10.
 case (H9 x0 ).
 case H6.
 auto.
 split;auto.
 case H6;auto.
 intro;subst y.
 inversion H6.
 case (lt_irr x0);auto.
 intro.
 case (lt_irr x0).
 apply lt_trans with y.
 case H6;eauto with schutte.
 auto.
Qed.

Lemma denumerable_segment_proper : forall A : Ensemble OT,
           O_segment A -> denumerable A -> proper_O_segment A.
Proof.
 intros.
 red.
 split;[auto|idtac].
 red;intro H1.
 generalize (Extensionality_Ensembles _ _ _ H1).
 intros; subst A.
 case Non_denum.
 auto.
Qed.

Definition ordering_function (f : OT -> OT)(A B : Ensemble OT) :=
 O_segment A /\
 (Included B ordinal) /\
 (forall a, In A a -> In B (f a)) /\
 (forall b, B b -> exists a, In A a /\ f a = b)/\
 forall a b , In A a -> In A b -> a < b -> f a < f b.

Definition ordering_function_segment (A B : Ensemble OT) :=
  exists f : OT -> OT, ordering_function f A B.

Definition ordering_segment_2_fun (A B : Ensemble OT) :=
   epsilon inh_OT_OT (fun f => ordering_function f A B).

Lemma ordering_segment_2_fun_ok :
  forall A B, ordering_function_segment A B ->
              ordering_function (ordering_segment_2_fun A B) A B.
Proof.
 intros A B H.
 pattern (ordering_segment_2_fun A B).
 unfold ordering_segment_2_fun.
 pattern (epsilon inh_OT_OT (fun f : OT -> OT => ordering_function f A B)).
apply epsilon_ind.
 case H.
 intros;exists x;auto.
 auto.
Qed.

Lemma ordering_function_ordA : forall f A B, ordering_function f A B ->
                                Included A ordinal.
 destruct 1.
 case H;auto.
Qed.
Hint Resolve ordering_function_ordA : schutte.

Lemma ordering_function_ordB : forall f A B, ordering_function f A B ->
                                Included B ordinal.
 destruct 1.
 tauto.
Qed.

Hint Resolve ordering_function_ordB : schutte.

Lemma Inc_elim : forall (U:Type) (A B: Ensemble U), Included A B -> forall a, In A a ->In B a.
 Proof.
 eauto.
Qed.
Hint Resolve Inc_elim: schutte.

Lemma ordering_function_mono : forall f A B, ordering_function f A B ->
   forall a b, In A a -> In A b -> a <b -> f a < f b.
Proof.
 destruct 1.
 tauto.
Qed.
Hint Resolve ordering_function_mono.

Lemma ordering_function_mono_weak :
 forall f A B, ordering_function f A B ->
   forall a b, In A a -> In A b -> a <= b -> f a <= f b.
Proof.
 destruct 1.
 decompose [and] H0; clear H0.
 destruct 3.
 case H6;intros; subst b.
left;
 auto with schutte.
 right;apply H5;auto.
Qed.
Hint Resolve ordering_function_mono_weak.

Lemma ordering_function_monoR : forall f A B, ordering_function f A B ->
   forall a b, In A a -> In A b -> f a < f b -> a < b.
Proof.
 intros.
 case H;
 intros.
 decompose [and] H4.
 clear H4.
 tricho a b H4.
 eapply (ordering_function_ordA H a H0 ).
  eapply (ordering_function_ordA H b H1 ).
 auto.
 subst b.
 case (lt_irr (f a)).
 auto.
 case (lt_irr (f a)).
 apply lt_trans with (f b);auto.
Qed.
Hint Resolve ordering_function_monoR.

Lemma Ordering_bijection : forall f A B, ordering_function f A B ->
                                        fun_bijection A B f.
Proof.
   destruct 1.
   decompose [and] H0; clear H0.
   split;red;auto.
   intros.
   tricho a a' H7.
   case H;intros H7 _; apply H7;auto.
   case H;intros H7 _; apply H7;auto.
   generalize (H5 _ _ H0 H4 ).
  rewrite H6; intro H8. case (lt_irr _ (H8 H7));auto.
  auto.
      generalize (H5 _ _ H4 H0 H7).
  rewrite H6; intro H8. case (lt_irr _ H8);auto.
 Qed.

Lemma ordering_function_mono_weakR :
 forall f A B, ordering_function f A B ->
   forall a b, In A a -> In A b -> f a <= f b -> a <= b.
Proof.
 intros.
 case H.
 intros. decompose [and] H4; clear H4.
 case H2;intros.
 case H4;intros.
 case (Ordering_bijection H).
 intros.
 case (H13 a b H0 H1 H10).
 left;split;auto with schutte.
 fold ordinal;eauto with schutte.
  right;auto.
 eapply ordering_function_monoR; eauto.
Qed.

Hint Resolve ordering_function_mono_weakR.

Lemma ordering_function_seg : forall A B, ordering_function_segment A B ->
                                          O_segment A.
Proof.
  destruct 1 as [ f Hf].
  case Hf;auto.
Qed.


Definition fun_eq (f g : OT -> OT )(A : OT -> Prop) :=
 forall a, In A a -> f a = g a.

Definition fun_eq_gen (f g : OT -> OT)(A B : OT -> Prop) :=
  Same_set A B /\ forall a, In A a -> f a = g a.

Lemma fun_eq_refl : forall (f : OT -> OT)(A : Ensemble OT),
   fun_eq_gen f f A A.
Proof.
 split; auto.
 split;auto.
Qed.

Definition fun_restrict (f g : OT -> OT)(A B : OT -> Prop) :=
  Included A B /\ forall a, In A a -> f a = g a.

Lemma empty_ordering : forall B, (forall b, ~ B b) ->
                                 ordering_function (fun o => o)
                                                   (members zero)
                                                   B.
Proof.
 intros.
 split.
 intros.
 split.
 red.
 destruct 1.
 red in H1.
 case (not_lt_zero x);auto.
 destruct 1.
  case (not_lt_zero x);auto.
 repeat split.
  red;intro b.
  intro;case (H b);auto.
  destruct 1.
  case (not_lt_zero x);auto.
  intros b Hb;case (H b);auto.
 intros a b Hb; case (not_lt_zero a).
 case Hb;auto.
Qed.

Lemma O_segment_ordinal : forall A a, O_segment A -> A a -> ordinal a.
Proof.
 intros.
 case H.
 intros.
 apply H1;auto.
Qed.

Lemma O_segment_lt : forall A a b, O_segment A -> A a -> b < a -> A b.
Proof.
 intros.
 case H;intros.
 apply H3 with a;auto.
Qed.

Hint Resolve O_segment_ordinal.


Theorem ordering_le : forall f A B, ordering_function f A B ->
  forall a, A a -> a <= f a.
Proof.
 intros.
 generalize H0; pattern a; apply Induction.
 2: case H; intuition.
 2: case H1.
 2:eauto with schutte.
 unfold ordering_function in H; decompose [and] H.
 clear H.
 unfold progressive.
 intros.
 tricho a0 (f a0) H'; auto with schutte.
 apply H3.
 auto.
 assert (f (f a0) < f a0).
 apply H6.
 eapply O_segment_lt;eauto with schutte.
 unfold In;auto.
 unfold In;auto.
 auto.
  case (le_not_gt (a:= f a0)(b:=f (f a0)));auto.
 apply H5; eauto with schutte.
 eapply O_segment_lt;eauto with schutte.
Qed.

Section ordering_function_unicity.
 Variables B A1 A2 : Ensemble OT.

 Variables f1 f2 : OT -> OT.
 Hypothesis O1 : ordering_function f1 A1 B.
 Hypothesis O2 : ordering_function f2 A2 B.

 Remark ord_B : Included B ordinal.
 Proof.
  case O1; intuition.
 Qed.



 Remark SA1 : O_segment A1.
 Proof.
  case O1;intuition.
 Qed.

 Remark SA2 : O_segment A2.
 Proof.
  case O2;intuition.
 Qed.

 Hint Resolve SA2 SA1 ord_B.

 Lemma A1_A2 :forall a, In A1 a -> A2 a /\ f1 a = f2 a.
 Proof.
  intros a Ha.
  generalize Ha;pattern a; apply Induction.
  2:apply O_segment_ordinal with A1;auto.
  clear a Ha.
  unfold progressive;intros.
  assert (A2 a).
  assert (forall khi, khi < a -> A2 khi /\ f1 khi = f2 khi).
  intros.
  apply H0.
  eauto with schutte.
  auto.
  apply O_segment_lt with a;auto.
  apply NNPP.
  red; intro.
  assert (forall y, A2 y -> y < a).
  intros.
  tricho y a H4.
  eauto with schutte.
  auto.
  subst y; case H2;auto.
  case H2.
  apply O_segment_lt with y;auto.
  assert (forall y, A2 y -> f1 y < f1 a).
  intros.
  case O1;intros.
  decompose [and] H6.
  apply H11;auto with schutte.
  case (H1 y).
  apply H3;auto.
  intros.
  apply O_segment_lt with a;auto.
  case O2;intros.
  decompose [and] H6.
  clear H6.
  case (H8 (f1 a)).
  case O1;intros.
  decompose [and] H10;clear H10.
  apply H14.
  auto.
  intro.
  destruct 1.
  generalize (H4 x H6).
  intro.
  case (H0 x).
  eauto with schutte.
  eauto with schutte.
  apply O_segment_lt with a;auto.
  intros.
  rewrite H14 in H12.
  rewrite H10 in H12.
  case (lt_irr (f1 a));auto.
  split.
  auto.
  assert (is_least_member (ordinal) lt (fun x => B x /\
                                                 forall y, y < a ->
                                                           f1 y <> x)
                          (f1 a)).
  split.
  case O1;intros.
  unfold In; intuition.
  apply H4.
  auto.
  split.
  split.
  case O1;intros.
  intuition.
  apply H3;auto.
  intros.
  red;intro.
  case (lt_irr (f1 a)).
  pattern (f1 a) at 1; rewrite <- H3.
  case O1;intros.
  decompose [and] H5.
  apply H10;auto with schutte.
  apply O_segment_lt with a;auto with schutte.
  destruct 2.
  case O1;intros.
  decompose [and] H6.
  case (H8 x H3).
  intros c (Hc,H'c).
  subst x.
  tricho (f1 c) (f1 a) H12.
  apply H7.
  auto.
  tricho c a H13.
  eauto with schutte.
  case (H4 c H13).
  auto.
  subst a;auto.
  right;apply H11;eauto with schutte.
  auto.
  auto.
  assert (is_least_member (ordinal) lt (fun x => B x /\ forall y, y < a ->
                                                         f2 y <> x)
                         (f2 a)).
  split.
  case O2;intros.
  case H4;auto.
  unfold In, Included;intuition.
  apply H7.
  auto.
  split.
  split.
  case O2;intros.
  intuition.
  apply H4;auto.
  intros.
  red;intro.
  case (lt_irr (f2 a)).
  pattern (f2 a) at 1; rewrite <- H4.
  case O2;intros.
  decompose [and] H6.
  apply H11;auto with schutte.
  apply O_segment_lt with a;auto with schutte.
  destruct 2.
  case O2;intros.
  decompose [and] H7.
  case (H9 x H4).
  intros c (Hc,H'c).
  subst x.
  tricho (f2 c) (f2 a) H13.
  apply H8.
  auto.
  tricho c a H14.
  eauto with schutte.
  case (H5 c H14).
  auto.
  subst a;auto.
  right;apply H12;eauto with schutte.
  auto.
  auto.
  eapply (least_member_unicity ON);eauto.
  generalize (least_member_of_eq ON
    (X:=fun x : M ON => B x /\
                        (forall y : M ON, y < a -> f2 y <> x))
    (Y:=fun x : M ON => B x /\ (forall y : M ON, y < a -> f1 y <> x)) ).
  intros.
  generalize (H4 (f2 a) (f1 a)).
  clear H4;intros.
  rewrite H4.
  auto.
  intros x (H5,H6).
  split;auto.
  intros.
  replace (f1 y) with (f2 y).
  auto.
  case (H0 y).
  eauto with schutte.
  auto.
  eapply O_segment_lt with a;auto.
  auto.
  intros x (H5,H6).
  split;auto.
  intros.
  replace (f2 y) with (f1 y).
  auto.
  case (H0 y).
  eauto with schutte.
  auto.
  eapply O_segment_lt with a;auto.
  auto.
  auto.
  auto.
Qed.

 Lemma A2_A1 :forall a, A2 a -> A1 a /\ f2 a = f1 a.
 Proof.
  intros a Ha.
  generalize Ha;pattern a; apply Induction.
  2:apply O_segment_ordinal with A2;auto.
  clear a Ha.
  unfold progressive;intros.
  assert (A1 a).
  assert (forall khi, khi < a -> A1 khi /\ f2 khi = f1 khi).
  intros.
  apply H0.
  eauto with schutte.
  auto.
  apply O_segment_lt with a;auto.
  apply NNPP.
  red; intro.
  assert (forall y, A1 y -> y < a).
  intros.
  tricho y a H4.
  eauto with schutte.
  auto.
  subst y; case H2;auto.
  case H2.
  apply O_segment_lt with y;auto.
  assert (forall y, A1 y -> f2 y < f2 a).
  intros.
  case O2;intros.
  decompose [and] H6.
  apply H11;auto with schutte.
  case (H1 y).
  apply H3;auto.
  intros.
  apply O_segment_lt with a;auto.
  case O1;intros.
  decompose [and] H6.
  clear H6.
  case (H8 (f2 a)).
  case O2;intros.
  decompose [and] H10;clear H10.
  apply H14.
  auto.
  intro.
  destruct 1.
  generalize (H4 x H6).
  intro.
  case (H0 x).
  eauto with schutte.
  eauto with schutte.
  apply O_segment_lt with a;auto.
  intros.
  rewrite H14 in H12.
  rewrite H10 in H12.
  case (lt_irr (f2 a));auto.
  split.
  auto.
  assert (is_least_member (ordinal) lt
                          (fun x => B x /\ forall y, y < a ->
                                                    f2 y <> x)
                          (f2 a)).
  split.
  case O2;intros.
  unfold In; intuition.
  apply H4.
  auto.
  split.
  split.
  case O2;intros.
  intuition.
  apply H3;auto.
  intros.
  red;intro.
  case (lt_irr (f2 a)).
  pattern (f2 a) at 1; rewrite <- H3.
  case O2;intros.
  decompose [and] H5.
  apply H10;auto with schutte.
  apply O_segment_lt with a;auto with schutte.
  destruct 2.
  case O2;intros.
  decompose [and] H6.
  case (H8 x H3).
  intros c (Hc,H'c).
  subst x.
  tricho (f2 c) (f2 a) H12.
  apply H7.
  auto.
  tricho c a H13.
  eauto with schutte.
  case (H4 c H13).
  auto.
  subst a;auto.
  right;apply H11;eauto with schutte.
  auto.
  auto.
  assert (is_least_member (ordinal) lt
                          (fun x => B x /\ forall y, y < a ->
                                                     f1 y <> x)
                          (f1 a)).
  split.
  case O1;intros.
  case H4;auto.
  unfold In, Included;intuition.
  apply H7.
  auto.
  split.
  split.
  case O1;intros.
  intuition.
  apply H4;auto.
  intros.
  red;intro.
  case (lt_irr (f1 a)).
  pattern (f1 a) at 1; rewrite <- H4.
  case O1;intros.
  decompose [and] H6.
  apply H11;auto with schutte.
  apply O_segment_lt with a;auto with schutte.
  destruct 2.
  case O1;intros.
  decompose [and] H7.
  case (H9 x H4).
  intros c (Hc,H'c).
  subst x.
  tricho (f1 c) (f1 a) H13.
  apply H8.
  auto.
  tricho c a H14.
  eauto with schutte.
  case (H5 c H14).
  auto.
  subst a;auto.
  right;apply H12;eauto with schutte.
  auto.
  auto.
  eapply (least_member_unicity ON);eauto.
  generalize (least_member_of_eq ON
     (X:=fun x : M ON => B x /\
       (forall y : M ON, y < a -> f1 y <> x))
     (Y:=fun x : M ON => B x /\ (forall y : M ON, y < a -> f2 y <> x)) ).
  intros.
  generalize (H4 (f1 a) (f2 a)).
  clear H4;intros.
  rewrite H4.
  auto.
  intros x (H5,H6).
  split;auto.
  intros.
  replace (f2 y) with (f1 y).
  auto.
  case (H0 y).
  eauto with schutte.
  auto.
  eapply O_segment_lt with a;auto.
  auto.
  intros x (H5,H6).
  split;auto.
  intros.
  replace (f1 y) with (f2 y).
  auto.
  case (H0 y).
  eauto with schutte.
  auto.
  eapply O_segment_lt with a;auto.
  auto.
  auto.
  auto.
Qed.

Theorem ordering_function_unicity : fun_eq_gen f1 f2 A1 A2.
Proof.
 intros.

 split.
 split.
 intro.
 intro.

 case (A1_A2 H);auto.
 intros x0 H0;case (A2_A1 H0);auto.
 intros.
 case (A1_A2 H);auto.
Qed.

End ordering_function_unicity.

Lemma ordering_function_seg_unicity : forall A1 A2 B,
           ordering_function_segment A1 B ->
           ordering_function_segment A2 B -> A1 = A2.
Proof.
 destruct 1 as [f1 Hf1].
 destruct 1 as [f2 Hf2].
 apply Extensionality_Ensembles.
 assert (fun_eq_gen f1 f2 A1 A2).
eapply ordering_function_unicity;eauto.
 case H;auto.
Qed.

Definition proper_segment_of (B : Ensemble OT)(beta : OT): Ensemble OT :=
  fun alpha => B alpha /\ alpha < beta /\ B beta.

Lemma proper_segment_ordinals : forall (B : OT -> Prop),
   (Included B ordinal) ->
    forall beta, In B beta -> Included (proper_segment_of B beta) ordinal.
Proof.
 intros B H beta Hbeta alpha Halpha.
 case Halpha.
 intros; apply H.
 auto.
Qed.


Section ordering_function_ex_recur.
 Variable B : Ensemble OT.

 Hypothesis OrdB : Included B ordinal.


 Variable recur : forall beta, In B beta ->
                               exists A : Ensemble OT,
                                    ordering_function_segment A
                                             (proper_segment_of B beta).

 Section beta_fixed.

 Variable beta : OT.
 Hypothesis beta_B : In B beta.

 Remark O_beta : ordinal beta.
 Proof.
   apply OrdB;auto.
 Qed.

let us build an ordering function for (proper_segment_of B beta)


 Definition _A := iota inh_Ordinal_sets (fun E => ordering_function_segment E
                                         (proper_segment_of B beta)).

Definition f_beta := epsilon inh_OT_OT
                        (fun f =>
                          ordering_function f _A
                           (proper_segment_of B beta)).

Lemma of_beta' : ordering_function f_beta _A (proper_segment_of B beta).

 pattern f_beta.
 hilbert_e.
 pattern _A.
 hilbert_e.
 case (recur beta_B).
 intros.
 exists x;split;auto.
 intros;eapply ordering_function_seg_unicity;eauto.
Qed.

 Remark Bbeta_denum : denumerable (proper_segment_of B beta).
 Proof.
  apply AX2.
  apply proper_segment_ordinals;auto.
  exists beta.
  split;auto.
  apply OrdB;auto.

  destruct 1;auto.
  destruct H0;auto.
 Qed.

Hint Resolve of_beta': schutte.

Remark A_denum : denumerable _A.
Proof.
 eapply denumerable_bij_funR.
  eapply Ordering_bijection.
 eauto with schutte.
 apply Bbeta_denum;eauto.
Qed.

Lemma Proper_A : proper_O_segment _A.
 apply denumerable_segment_proper.
 eapply SA1.
 eauto with schutte.
 eapply A_denum.
Qed.

Lemma g_def1 : exists g_beta, ordinal g_beta /\ _A = members g_beta.
 generalize (proper_members Proper_A).
 intros (a,Ha);exists a;split.
 case Ha;auto.
 eapply Extensionality_Ensembles.
 auto.
 case Ha;auto.
Qed.

Lemma g_unic : forall g_beta g_beta', ordinal g_beta ->
                                      ordinal g_beta' ->
                                      _A = members g_beta ->
                                      _A = members g_beta' ->
                                      g_beta = g_beta'.
Proof.
  intros.
  rewrite H2 in H1;clear H2.
  assert (Same_set (members g_beta') (members g_beta)).
  rewrite H1;auto.
 split;auto.
 case H2.
 unfold Included, members; intros.
 apply le_antisym.
 apply not_gt_le; auto with schutte.
 red.
 intro.
 generalize (H4 g_beta').
 intros.
 unfold In in H6.
 case (lt_irr g_beta').
 assert (Intersection OT ordinal (fun b : OT => b < g_beta) g_beta').
 split;auto.
 generalize (H6 H7).
 intro.
 inversion H8.
 auto.
 apply not_gt_le; auto with schutte.
 red.
 intro.
 generalize (H3 g_beta).
 intros.
 unfold In in H6.
 case (lt_irr g_beta).
 assert (Intersection OT ordinal (fun b : OT => b < g_beta') g_beta).
 split;auto.
 generalize (H6 H7).
 intro.
 inversion H8.
 auto.
Qed.

Definition g := iota inh_OT (fun o => ordinal o /\ _A = members o).

End beta_fixed.

Lemma g_def : forall beta, In B beta -> _A beta = members (g beta ).
Proof.
 intros.
 pattern (g beta).
 hilbert_e.
 case (g_def1 H).
 intros x (Hx,H'x).
 exists x.
 split;auto.
 intros a' (Ha',Ha'').
 eapply g_unic;eauto.
 tauto.
Qed.

Lemma g_ord : forall beta, In B beta -> ordinal (g beta).
Proof.
  intros.
 pattern (g beta).
  hilbert_e.
 case (g_def1 H).
 intros x (Hx,H'x).
 exists x;split;auto.
 intros a' (Ha',Ha'').
 eapply g_unic;eauto.
 tauto.
Qed.

Lemma g_domains : fun_codomain B ordinal g.
Proof.
 red.
 exact g_ord.
Qed.

Lemma g_lemma :
  forall beta, In B beta ->
       ordering_function (f_beta beta) (members (g beta))
                                       (proper_segment_of B beta).
Proof.
 intros.
 rewrite <- g_def.
 apply of_beta'.
 auto.
 auto.
Qed.

Lemma g_mono : forall beta1 beta2, In B beta1 -> In B beta2 ->
                                   beta1 < beta2 ->
                                   g beta1 < g beta2.

 intros.

 assert( B2 : fun_bijection (members (g beta2)) (proper_segment_of B beta2) (f_beta beta2)) .
 apply Ordering_bijection.
 apply g_lemma; auto.

 assert (B3 : In (proper_segment_of B beta2) beta1).

 red;red.
 split; auto.

 assert (B4 : exists alpha, ordinal alpha /\ alpha < g beta2 /\ f_beta beta2 alpha= beta1).

 case B2.
 intros.
 case (H3 beta1).
 auto.
 intros alpha (H5,H6).
 exists alpha.
 split;auto.
 case H5;auto.
 split;auto.
 case H5;auto.
 case B4; intros alpha (Ha1,(Ha2,Ha3)).
 assert (B5 : ordering_function (f_beta beta2) (members alpha)
                 (proper_segment_of B beta1)).
repeat split;auto with schutte.

 red;destruct 1;auto.
 cbv beta delta[In].
 eauto with schutte.
 red;apply lt_trans with a;eauto.

 case H2;auto.
 red.
 destruct 1;auto.

 case B2;intros.
 clear H4 H5.
 red in H3.
 generalize (H3 a).
 intros.
 clear H3.
 case H4.
 2:auto.
 split.
 case H2;auto.
 red.
 apply lt_trans with alpha.
 case H2;auto.
 auto.
 case (g_lemma H0).
 intros.
 decompose [and] H4.
 clear H4.
 replace beta1 with (f_beta beta2 alpha).
 apply H9;auto.
 split.
 case H2;auto.
 red.
 apply lt_trans with alpha;auto.
 case H2;auto.
  split;auto.
 case H2;auto.
 destruct 1.
case (g_lemma H0).
  intros.
 decompose [and] H4.
 clear H4.
decompose [and] H5.
 clear H9.
clear H7.
clear H5.

 case (H6 b).
 split;auto.
split;auto.
 eapply lt_trans;eauto.
 case H3;auto.

 intros a (Ha,Ha');exists a;split;auto.
 split.
 case Ha;auto.
 red.
 tricho a alpha X.
 case Ha;auto.
 auto.
 subst a.
 rewrite Ha3 in Ha'.
 subst b.
 case H3;intros H33 _.
case (lt_irr _ H33).
 clear H6.
 assert (beta1 < b).
 rewrite <- Ha3; rewrite <- Ha'.
 case (g_lemma H0).
 destruct 1.

 intros.
 decompose [and] H7.
 apply H12;auto.
 split;auto.
 case (lt_irr beta1).
 apply lt_trans with b;auto.
 case H3;auto.
 intros.

  case (g_lemma H0).
 destruct 1.
 intros.
 decompose [and] H7.
 apply H12;auto.
 clear H10 H9 H12 H7.
 split;auto.
 case H2;auto.
 red.
 apply lt_trans with alpha;auto.

 case H2;auto.
 split;auto.


 case H3;auto.
 red.
 apply lt_trans with alpha;auto.

 case H3;auto.

 generalize (g_lemma H);intro.
generalize (ordering_function_unicity B5 H2).
 destruct 1.
 generalize (Extensionality_Ensembles _ _ _ H3).
 intros.
 generalize (members_eq Ha1 (g_ord H) H5).
 intro; subst alpha;auto.
Qed.

Lemma L3a : O_segment (image B g).
Proof.
 split.
 red.
 intro a;destruct 1.
 case H.
 intros; subst a.
 red;apply g_ord;auto.
 intros gbeta alpha (beta,(H1,H2)) H3.
 assert (Halpha : ordinal alpha) . ordi.
 subst gbeta.
 red.
 generalize (g_lemma H1);intro.
 case H; intros.
 decompose [and] H2;clear H2.
 assert (exists beta0, In (proper_segment_of B beta) beta0
                      /\ f_beta beta alpha=beta0).
 exists (f_beta beta alpha).
 split;auto.
 apply H6.
 split;auto.

 case H2;intros beta0 (H9,H10).
 clear H2.

assert (B5 : ordering_function (f_beta beta) (members alpha)
                 (proper_segment_of B beta0)).

repeat split;auto with schutte.
red; destruct 1;auto.
 cbv beta delta[In].
  eauto with schutte.
red;
apply lt_trans with a;eauto.
 case H2;auto.
 red.
 destruct 1;auto.
 assert( B2 : fun_bijection (members (g beta)) (proper_segment_of B beta) (f_beta beta)) .
 apply Ordering_bijection.
 apply g_lemma; auto.


 case B2;intros.
 red in H7.
 generalize (H7 a).
 intros.
 clear H7.
 case H13.
 2:auto.

 split.

 case H2;auto.
 red.
 apply lt_trans with alpha.
 case H2;auto.
 auto.

 case (g_lemma H1).
 intros.
 decompose [and] H11.
 clear H11.
 replace beta0 with (f_beta beta alpha).
 apply H16;auto.
 split.
 case H2;auto.
 red.
 apply lt_trans with alpha;auto.
 case H2;auto.
  split;auto.
 case H2;auto.
 case H9.
 auto.
 destruct 1.
case (g_lemma H1).
  intros.
 decompose [and] H11.
 clear H11.
decompose [and] H12.
 case (H13 b).
 split;auto.
  split;auto.

apply lt_trans with beta0;auto.

 case H7;auto.
 case H9;auto.

 destruct 2; auto.
 intros a (Ha,Ha');exists a;split;auto.

 split.
 case Ha;auto.
 red.
 tricho a alpha X.
 case Ha;auto.
 auto.
 subst a.
 rewrite H10 in Ha'.

 subst b;case H7; intros H77 _.
 case (lt_irr _ H77).
 assert (beta0 < b).
 rewrite <- H10; rewrite <- Ha'.
 case (g_lemma H1).
 destruct 1.
 intros.
 decompose [and] H18.
 apply H23;auto.
 split;auto.
 case (lt_irr beta0).

 apply lt_trans with b;auto.
 case H7;auto.
 intros.
  case (g_lemma H1).
 destruct 1.
 intros.

 decompose [and] H14.
 apply H19;auto.
 split;auto.
 case H2;auto.
 red.
 apply lt_trans with alpha;auto.

 case H2;auto.
 split;auto.


 case H7;auto.
 red.
 apply lt_trans with alpha;auto.

 case H7;auto.


 generalize (g_lemma (beta:=beta0));intros.
 case H9;intros.
 generalize (H2 H7).
 intros.
generalize (ordering_function_unicity B5 H12).
 destruct 1.
 generalize (Extensionality_Ensembles _ _ _ H13).

 intros.

 generalize (members_eq (a:=alpha)(b:=g beta0) Halpha (g_ord H7) H15 ).
 intro.
 exists beta0.
 split;auto.
Qed.

 Lemma g_bij : fun_bijection B (image B g) g.
 split.
 red.
 intros.
 red;red.
 exists a;split;auto.
 red.
 destruct 1.
 exists x;split;auto.
 case H;auto.
 case H;auto.
 red;intros.
 tricho a a' XXX.
 apply OrdB;auto.
 apply OrdB;auto.
 generalize (g_mono H H0 XXX).
 intro.
 rewrite H1 in H2.
 case (lt_irr _ H2).
 auto.
generalize (g_mono H0 H XXX).
 intro.
rewrite H1 in H2.
 case (lt_irr _ H2).
 Qed.

 Hint Resolve g_bij : schutte.

Let g_1 := inv_fun inh_OT B (image B g) g.

Lemma g_1_bij : fun_bijection (image B g) B g_1.
Proof.
 unfold g_1.
 apply inv_fun_bij; auto with schutte.
Qed.

Hint Resolve g_1_bij : schutte.

Lemma g_1_of : ordering_function g_1 (image B g) B.

 split.
 apply L3a.
 repeat split.
 auto.
 destruct 1.
 case H.
 intros.
 rewrite <- H1.
 replace (g_1 (g x)) with x.
 auto.
 symmetry;unfold g_1;eapply inv_compose;eauto.
 auto with schutte.
 auto with schutte.

intros.
 exists (g b).
 split;auto.
 exists b.
 split;auto.
 unfold g_1;eapply inv_compose;eauto.
 auto with schutte.
 auto with schutte.
 intros.

 tricho (g_1 a) (g_1 b) XXX; auto with schutte.
 case g_1_bij; intros.
 generalize (H2 a H).
 intros;apply OrdB;auto.
  case g_1_bij; intros.
generalize (H2 b H0).
 intros;apply OrdB;auto.
 replace a with (g (g_1 a)) in H1.
 replace b with (g (g_1 b)) in H1.
 rewrite XXX in H1.
 case (lt_irr _ H1).
 unfold g_1;
 apply inv_composeR;
 auto with schutte.

unfold g_1;
 apply inv_composeR;
 auto with schutte.
 case (le_not_gt (a:=a)(b:= b)).
 auto with schutte.
 replace a with (g (g_1 a));
 replace b with (g (g_1 b)) .
 apply g_mono;auto with schutte.
 case g_1_bij;auto with schutte.
 case g_1_bij;auto with schutte.
 unfold g_1;
 apply inv_composeR;
 auto with schutte.
unfold g_1;
 apply inv_composeR;
 auto with schutte.

 unfold g_1;
 apply inv_composeR;
 auto with schutte.
Qed.

Lemma L3 : exists AB, ordering_function_segment AB B.
 exists (image B g).
 exists g_1.
 apply g_1_of.
Qed.

Lemma L3' : exists AB, exists f, ordering_function f AB B.
  exists (image B g).
 exists g_1.
 apply g_1_of.
Qed.

End ordering_function_ex_recur.

Section ofB.
 Variable B : Ensemble OT.
 Hypothesis OB : Included B ordinal.

 Theorem B_of : exists AB, ordering_function_segment AB B.
 apply L3.
 auto.
 intros beta Hbeta; pattern beta; apply Induction.

 red.
 intros.
 apply L3.
 red; destruct 1;auto.
 intros.
 case H1;intros H2 (H3,H4).
 replace (proper_segment_of (proper_segment_of B a) beta0)
  with (proper_segment_of B beta0).

 apply H0.
 apply OB;eauto.
 auto.

 apply Extensionality_Ensembles; split.
 red; destruct 1; auto.
 red.
 red.
 case H6;intros;repeat split;auto.
 eapply lt_trans;eauto.

red; destruct 1;auto.
 red.

 case H6;intros;repeat split;auto.
 case H5;auto.
 apply OB;auto.
Qed.

Theorem B_of' : exists AB, exists f, ordering_function f AB B.
Proof.
 case B_of;intros AB (f,pi).
 eauto.
Qed.

Definition the_ordering_segment := epsilon inh_Ordinal_sets
                               (fun x => ordering_function_segment x B).

Definition the_ordering_function :=
   epsilon inh_OT_OT
   (fun f => ordering_function f the_ordering_segment B).

Lemma the_ordering_function_ok :
 ordering_function the_ordering_function the_ordering_segment B.
Proof.
 pattern the_ordering_function.
 hilbert_e.
 pattern the_ordering_segment.
 hilbert_e.
 case B_of.
 intros.
 exists x.
 auto.
Qed.

 Lemma the_ordering_function_eq : forall A f,
    ordering_function f A B -> fun_eq_gen f the_ordering_function
                                          A the_ordering_segment.
 Proof.
   intros;eapply ordering_function_unicity.
    eauto.
    apply the_ordering_function_ok.
 Qed.

End ofB.

Lemma ordering_function_ordinal_B : forall A B f,
          ordering_function f A B -> forall a, In A a -> ordinal (f a).
Proof.
  intros.
  case H.
  destruct 2.
  decompose [and] H3.
  generalize (H2 _ (H4 a H0)).
 auto.
Qed.

Lemma of_image : forall f A B, ordering_function f A B ->
                               ordering_function f A (image A f).
Proof.
 intros f A B O; case O; intros.
 decompose [and] H0.
 repeat split;auto.
 case H;auto.
 case H;auto.
 red.
 destruct 1.
 apply H1.
 decompose [and] H4.
 subst x;apply H3.
 auto.
 intros; exists a;auto.
Qed.

Section Th13_5.
 Variables (A B : Ensemble OT).
 Variable f : OT -> OT.
 Hypothesis f_ord : ordering_function f A B.

 Section recto.

 Hypothesis f_cont : continuous f A B.

 Section M_fixed.
 Variable M : Ensemble OT.
 Hypothesis inc : Included M B.
 Hypothesis ne : Inhabited _ M.
 Hypothesis den : denumerable M.

 Let U := fun u => In A u /\ In M ( f u).

 Remark fbij : fun_bijection A B f.
  apply Ordering_bijection.
  auto.
 Qed.


 Remark restrict : fun_bijection U M f.
 Proof.
   split.
   red.
   destruct 1;auto.
   red.
   case fbij.
   intros.
  case (H0 b).
  apply inc;auto.
 intros x (Hx,H'x).
 exists x;split;auto.
 red;unfold U.
 split;auto.
 subst b;auto.
 red.
 destruct 1.
 destruct 1.
 intros.
 case fbij;intros.
 apply H6;auto.
Qed.

 Remark Inc_U_A : Included U A.
 red.
 destruct 1.
 auto.
 Qed.

 Remark den_U : denumerable U.
 eapply denumerable_bij_funR with OT M f;auto.
 apply restrict.
 Qed.

 Remark inh_U : Inhabited _ U.
 case ne;intros.
 exists (inv_fun inh_OT A B f x).
 red; unfold U.

  rewrite inv_composeR.
 split;auto.
 generalize (Ordering_bijection f_ord).
  intros.

 generalize (inv_fun_bij inh_OT H0).
 intros.
 case (H1 H0).
 intros.
 apply H2.
  apply inc;auto.
 apply Ordering_bijection; auto.
 apply inc;auto.
 Qed.


 Remark im_U_f : (image U f : Ensemble OT) = M.
 eapply Extensionality_Ensembles.
 split.
 red;destruct 1.
 unfold U in H.
 case H.
 intros.
 red in H0.
 case H0;intros.
 subst x;auto.
 red.
 intros.
 red.
 red.
 exists (inv_fun inh_OT A B f x).
 split.
 red;red.
  generalize (Ordering_bijection f_ord).
 intros.
 split.
 case (inv_fun_bij inh_OT H0).
 auto.
 intros.
 apply H1.
 apply inc;auto.
 rewrite inv_composeR; auto with schutte.
 apply inc;auto.
 rewrite inv_composeR; auto with schutte.
 apply Ordering_bijection;auto with schutte.
 apply inc;auto with schutte.
Qed.

 Lemma sup_M_in_B : In B (sup M).
 Proof.
  rewrite <- im_U_f.
  case f_cont.
  intros.
 rewrite H1; auto.
 apply H.
 case H0; intros.
 apply H3;auto.
 apply Inc_U_A.
 apply inh_U.
 apply den_U.
 apply Inc_U_A.
  apply inh_U.
apply den_U.
Qed.

End M_fixed.

Lemma Th_13_5_1 : closed B.
 split.
 eauto with schutte.
 apply sup_M_in_B.
 Qed.

End recto.

Section verso.
 Hypothesis B_closed : closed B.

 Section U_fixed.
 Variable U : Ensemble OT.
 Hypothesis U_non_empty : Inhabited _ U.
 Hypothesis U_den : denumerable U.
 Hypothesis U_inc_A : Included U A.

 Remark R1_aux : denumerable (image U f).
 Proof.
 apply denumerable_bij_fun with OT U f.
 case (Ordering_bijection f_ord).
 intros.
 split.
 intros u u_In_U.
 repeat red. exists u; auto.
 intros u u_In_img.
 case u_In_img.
 intros x Hx.
 exists x; assumption.
 intros u1 u2 u1_In_U u2_In_U Heq.
 apply H1; try apply U_inc_A; assumption.
 assumption.
 Qed.

 Definition R1 := let foo := U_den in R1_aux.
 Opaque R1.

 Remark R2 : In B (sup (image U f)).
 Proof.
   case B_closed.
 intros.
 apply H0;auto.
 red;red.
 destruct 1.
 case f_ord.
 intros _ (_,(H2,_)).
 case H1;intros.
 subst x;apply H2.
 apply U_inc_A;auto.
 case U_non_empty;intros.
 exists (f x);auto.
 red;red.
 exists x;auto.
 apply R1_aux.
Qed.

Remark R3: exists alpha, In A alpha /\ f alpha = sup(image U f).
Proof.
 case f_ord.
 intros.
 decompose [and] H0.
 case (H2 (|_|image U f)).
 apply R2.
 intros x; exists x;auto.
Qed.

Let alpha_ : OT.
 some_i (fun alpha => In A alpha /\ f alpha = sup(image U f)).
 auto with schutte.
 apply R3.
Defined.

Lemma alpha_A : In A alpha_.
Proof.
 pattern alpha_ . some_elim.
 tauto.
Qed.

Lemma alpha_sup : f alpha_ = sup(image U f).
Proof.
 pattern alpha_; some_elim.
 tauto.
Qed.

Remark R5 : forall khi, In U khi -> f khi <= f alpha_.
Proof.
 intros.
 rewrite alpha_sup.
 pattern (image U f),(|_|image U f).
 pfun_e.
 split.
 apply R1.
 red.
 destruct 1.
 decompose [and] H0.
 subst x.
 clear H0.
 case f_ord;intros.
 decompose [and] H2.
 apply H3; auto.
 destruct 1.
 destruct 1.
 decompose [and] H3.
 case (H4 (f khi)).
 case f_ord.
 intros.
 decompose [and] H7.
 generalize (H8 (f khi)).
 intros.
 apply H11.
 auto.
 red.
 exists khi.
 split;auto.
 left.
 split;auto.
 rewrite H6.
 auto.
 right;auto.
Qed.

Remark R6 : forall khi, In U khi -> khi <= alpha_ .
Proof.
 intros.
 case (R5 H).
 left.
 split.
 generalize (U_inc_A H).
 case f_ord .
 destruct 1.
 intros.
 fold ordinal. red; apply H1; auto.
 case (Ordering_bijection f_ord).
 intros.
 apply H3.
 apply U_inc_A;auto.
 apply alpha_A.
 case H0;auto.
 fold lt.
 right.
 fold lt .
 case f_ord.
 intros _ H1; decompose [and] H1.
 tricho khi alpha_ H7.
 generalize (U_inc_A H).
 intro.
 case f_ord.
 intros H11 _; case H11.
 intros.
 apply H7;auto.
 case f_ord.
 intros H11 _; case H11.
 intros.
 apply H5.
 apply alpha_A.
 auto.
 subst khi.
 case (lt_irr _ H0).
 case (lt_irr (f alpha_)).
 apply lt_trans with (f khi).
 apply H6;auto.
 apply alpha_A.
 auto.
Qed.

Remark R000 : forall a, In A a -> ordinal a.
Proof.
 case f_ord;intros.
 case H;intros.
 apply H2;auto.
Qed.
Hint Resolve R000.

Remark R001 : forall u, In U u -> ordinal u.
Proof.
 intros.
 assert (In A u).
 apply U_inc_A;auto.
 auto.
Qed.

Hint Resolve R001 alpha_A.

Remark R7 : sup U <= alpha_ .
 pattern U,(sup U); pfun_e.
 destruct 1.
 destruct 1.
 decompose [and] H2.
 case (H4 alpha_).
 auto.
 red.
 intros.
 case (R6 H6).
 tauto.
 tauto.
 left;auto.
 right;auto.
Qed.



Remark R4 : forall khi, In U khi -> khi <= sup U.
Proof.
 intros.
 pattern U,(sup U).
 pfun_e.
 destruct 1.
 destruct 1.
 case H3;intros H4 H5.
 case ( H4 khi);auto with schutte.
Qed.

Lemma A_closed : In A (sup U).
Proof.
 assert (O_segment A).
 eapply SA2.
 eauto.
 case H.
 intros.
 case R7.
 destruct 1;intros.
 rewrite H3.
 apply alpha_A.
 intros;red.
 eapply H1 with alpha_ ;auto.
apply alpha_A.
Qed.

Remark R4' : forall khi, In U khi -> f khi <= f (sup U).
Proof.
 intros.
 case f_ord;intros.
 decompose [and] H1.
 clear H1.
 case (R4 H).
 destruct 1.
 subst khi;left;auto with schutte.
 right;auto.
 apply H6;auto with schutte.
 apply A_closed;auto.
Qed.

Remark R4'' : sup (image U f) <= f (sup U).
Proof.
 pattern (image U f),(sup (image U f)).
 pfun_e.
 split;auto with schutte.
 apply R1.
 red;eauto with schutte.
 destruct 1.
 case H.
 intros.
 subst x.
 clear H.
 case f_ord;intros.
 decompose [and] H1.
 apply H2.
 apply H4;auto.
 destruct 1.
 intros (H'1,H1).
 decompose [and] H1.
 case (H3 (f (sup U))).
 case f_ord;intros.
 decompose [and] H5.
 generalize (H6 (f (sup U))).
 intros.
 apply H9.
 apply H8.
 apply A_closed;auto.
 red.
 intros.
 case H5;intros.
 decompose [and] H6.
 subst x.
 clear H6.
 case (R4' H7).
 tauto.
 fold lt;auto.
 auto with schutte.
 auto with schutte.
Qed.

Remark R42 : f(sup U) <= sup (image U f).
Proof.
 apply le_trans with (f alpha_).
 case f_ord;intros.
 decompose [and] H0;clear H0.
 case R7.
 destruct 1.
 rewrite H4;auto with schutte.
 left.
 split;auto.
 right;auto.
 apply H5;auto.
 apply A_closed;auto.
 pattern alpha_.
 some_elim.
 destruct 1.
 left;auto.
 split;auto.
 case f_ord.
 intros.
 decompose [and] H2.
 fold ordinal.
 apply H3.
 auto.
Qed.

Lemma f_sup_commutes : f (sup U)=sup (image U f).
Proof.
 apply le_antisym.
 apply R42.
 apply R4''.
Qed.

End U_fixed.

Lemma Th_13_5_2 : continuous f A B.
Proof.
 split.
 red.
 case f_ord;tauto.
 split.
 case f_ord;intros.
 case H;auto.
 intros;apply A_closed;auto.
 intros;symmetry;apply f_sup_commutes;auto.
Qed.

End verso.

End Th13_5.

Inductive normal (f : OT -> OT)(B : Ensemble OT): Prop :=
normal_intro : ordering_function f ordinal B ->
               continuous f ordinal B ->
               normal f B.

Theorem TH_13_6 : forall B f, Included B ordinal ->
                              normal f B ->
                              closed B /\ Unbounded B.
Proof.
 destruct 2.
 split.
 eapply Th_13_5_1;eauto.
 red.
 intros.
 generalize (Ordering_bijection H0).
 destruct 1.
 exists (f (succ x)).
 split.
 apply H3.
 red.
 auto with schutte.
 apply le_lt_trans with (f x).
 eapply ordering_le;eauto.
 eapply ordering_function_mono;eauto.
 red.
 auto with schutte.
 auto with schutte.
Qed.

Theorem O_segment_unbounded : forall (A:Ensemble OT), O_segment A ->
                                        Unbounded A ->
                                        A = ordinal.
Proof.
 intros.
 red in H0.
 apply Extensionality_Ensembles.
 split.
 case H.
 red;auto.
 red.
 intro.
 intro;case (H0 x).
 auto.
 destruct 1.
 case H;intros.
 red;eapply H5;eauto.
 auto.
Qed.

Lemma ordering_unbounded_unbounded :
  forall A B f, Included B ordinal -> ordering_function f A B ->
                                  (Unbounded B <-> Unbounded A).
Proof.
 split;intros.
 apply not_denumerable_unbounded.
 case H0.
 intros H2 _;auto with schutte.
 red.
 case H2.
 auto.
 red;intro.
 assert (denumerable B).
 apply denumerable_bij_fun with OT A f;auto.
 auto with schutte.
 apply Ordering_bijection;auto.
 case (denumerable_not_Unbounded H H3);auto.
 apply not_denumerable_unbounded.
 auto.
 red;intro.
 assert (denumerable A).
 apply denumerable_bij_funR with OT B f;auto.
 apply Ordering_bijection;auto.
 case (denumerable_not_Unbounded (X:= A));auto.
 case H0.
 destruct 1;auto.
Qed.

Theorem TH_13_6R : forall A B f, Included B ordinal ->
                                 ordering_function f A B ->
                                 closed B ->
                                 Unbounded B ->
                                 normal f B.
Proof.
 intros.
 assert (A = ordinal).
 apply O_segment_unbounded.
 eapply SA1;eauto.
 case (ordering_unbounded_unbounded H H0).
 tauto.
 split.
 subst A ;auto.
 apply Th_13_5_2.
 subst A;auto.
 auto.
Qed.

Lemma order_function_least_least :
 forall B f , ordering_function f ordinal B ->
     is_least_member ordinal lt B (f zero).
Proof.
 intros.
 case H ;intros.
 decompose [and] H1; clear H1.
 case H.
 intros H8 (H9,H10).
 split.
 apply H2.
 apply H4;auto.
 red;auto with schutte.
 split.
 apply H4;auto.
 red;auto with schutte.
 intros.
 decompose [and] H10.
 case (H12 _ H5).
 intros x0 (Hx0,H'x0).
 subst x.
 generalize (ordering_function_mono_weak H (a:=zero) (b:=x0)).
 intros.
 case H11;auto with schutte.
 destruct 1;auto.
Qed.

Lemma O_segment_lt_closed : forall A a b, O_segment A ->
                                          In A b ->
                                          a < b ->
                                          In A a.
Proof.
 intros.
 case H.
 intros.
 red;auto.
 eapply H3.
 2:eauto.
 auto.
Qed.