Library schutte.AP

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

Require Import Arith.
Require Import Epsilon.
Require Import Ensembles.
Require Import Denumerable.
Require Import Schutte.
Require Import Ordering_Functions.
Require Import PartialFun.

Require Import Plus.
Require Import Well_Orders.

Set Implicit Arguments.

Inductive AP (alpha : OT) : Prop :=
 AP_intro : zero < alpha -> (forall beta, beta < alpha ->
                                              beta + alpha = alpha) ->
                AP alpha.

Lemma not_AP_inv : forall alpha,
                    zero < alpha ->
                    ~ (AP alpha) ->
                    exists beta,zero < beta /\ beta < alpha /\ alpha < beta + alpha .
 intros.
 apply Classical_Prop.NNPP.
 red;intro;apply H0.
 split.
 auto.
 intros.
 tricho (beta+alpha) alpha H3.
 eauto with schutte.
 eauto with schutte.
 case (lt_irr alpha).
 apply le_lt_trans with (beta+alpha).
 apply le_plus_r;eauto with schutte.
 auto.
 auto.
 case H1.
 exists beta;auto.
 split;auto.
 tricho zero beta H4. eauto with schutte.
 auto.
 subst beta.
 rewrite zero_plus_alpha in H3.
 case (lt_irr alpha);auto.
 eauto with schutte.
 case (not_lt_zero beta).
 eauto with schutte.
Qed.

Lemma not_AP_inv2 : forall alpha, zero < alpha -> ~AP alpha ->
                               exists beta, exists gamma,
                                     zero < beta /\ zero < gamma /\
                                     beta < alpha /\ gamma < alpha /\
                                      alpha = beta + gamma.
Proof.
 intros.
 case (not_AP_inv H H0).
 intros khi (Hkhi, H'khi).
 exists khi.
 case (minus_exists (alpha:=khi) (beta:= alpha)).
 eauto with schutte.
 case H'khi;eauto with schutte.
 intros eta (H1,H2).
 exists eta.
 split.
 auto.
 split;auto.
 tricho zero eta H3.
 auto.
 subst eta.
 rewrite alpha_plus_zero in H2.
 decompose [and] H'khi.
 subst alpha; case (lt_irr khi);auto.
  eauto with schutte.
 case (not_lt_zero eta);eauto with schutte.
 decompose [and] H'khi.
 split;auto.
 split;auto.
 tricho zero khi H5.
 eauto with schutte.
  tricho eta alpha H6. eauto with schutte.
 auto. subst eta.
 case (lt_irr (khi+alpha));eauto with schutte.
 case (lt_irr (khi + eta));eauto with schutte.
 apply lt_trans with (khi+alpha);eauto with schutte.
 apply plus_mono_r;eauto with schutte.
  subst khi.
 case (lt_irr zero);auto.
 case (not_lt_zero khi);eauto with schutte.
Qed.


Lemma AP_one : AP (F 1).
Proof.
  split.
  simpl (F 1).
  auto with schutte.
  simpl (F 1).
  intros.
  assert (beta <= zero).
  eapply lt_succ_le_2;eauto with schutte.
  rewrite (le_alpha_zero H0).
  rewrite zero_plus_alpha;eauto with schutte.
Qed.

Lemma least_AP :is_least_member ordinal lt AP (F 1).
Proof.
 split.
 red;auto with schutte.
 split.
 red;apply AP_one.
 intros.
 case H0.
 intros.
 tricho x (F 1) H3; auto with schutte.
 simpl (F 1) in H3.
 assert (x = zero).
 apply le_alpha_zero;auto with schutte.
 apply lt_succ_le_2;eauto with schutte.
 subst x.
 case (lt_irr zero); auto.
Qed.


Lemma AP_omega : AP omega.
Proof.
 repeat split.
 apply lt_trans with (F 1).
 simpl (F 1); eauto with schutte.
 apply finite_lt_omega.
 intros.

case (lt_omega_finite _ H).
intros;subst beta.
apply finite_plus_ge_omega;eauto with schutte.
Qed.

Lemma zero_lt_omega : zero < omega.
Proof.
  apply lt_trans with (F 1). eauto with schutte.
  apply finite_lt_omega;auto.
Qed.

Hint Resolve zero_lt_omega : schutte.

Lemma AP_finite_eq_one : forall n, AP (F n) -> n = 1.
Proof.
 intro n; case n.
 inversion 1.
 simpl in H0.
 case (lt_irr zero);auto.
 intro n0;case n0.
 auto.
 inversion_clear 1.
 generalize (H1 (F 1)).
 intros.
 absurd (F 1 + F S (S n1) = F S (S n1)).
 rewrite <- plus_FF.
  simpl.
 red;intro.
 case (lt_irr (succ (succ (F n1)))).
 pattern (succ (succ (F n1))) at 2; rewrite <- H2.
 auto with schutte.
 apply H.
 apply finite_mono.
 auto with arith.
Qed.

Lemma omega_second_AP : is_least_member ordinal lt
                                        (fun alpha => (F 1 < alpha) /\ AP alpha)
                                         omega.
Proof.
 split.
 red; auto with schutte.
 split; auto with schutte.
 red; split.

 apply finite_lt_omega.
 apply AP_omega.
 intros.
 red in H0.
 tricho x (omega) H1;auto with schutte.
 case (lt_omega_finite _ H1).
 intros; subst x.
 decompose [and] H0.
 generalize (AP_finite_eq_one _ H3).
 intro;subst x0.
 case (lt_irr (F 1)).
 auto.
Qed.



Lemma AP_plus_closed : forall alpha, AP alpha ->
                                 forall beta gamma, beta < alpha ->
                                                    gamma < alpha ->
                                                    beta + gamma < alpha.
Proof.
 intros.
 case H.
 intros.
 generalize (plus_mono_r beta gamma alpha).
 intro.
 replace alpha with (beta+alpha).
 apply H4; eauto with schutte.
 auto.
Qed.

Section AP_Unbounded.
 Variable alpha : OT.
 Hypothesis o_alpha : ordinal alpha.

 Let seq := (fix seq (n:nat) :=
               match n with 0 => succ alpha
                          | S p => (seq p) + (seq p)
               end).


 Let beta := omega_limit seq.

 Remark mono_seq : forall i, seq i < seq (S i).
  induction i.
  simpl.
  pattern (succ alpha) at 1.
  rewrite <- alpha_plus_zero.
  2:eauto with schutte.
  apply plus_mono_r; eauto with schutte.
  simpl.
  simpl in IHi.

  pattern (seq i + seq i) at 1; rewrite <- alpha_plus_zero;auto with schutte.
  apply plus_mono_r. eauto with schutte.
  apply le_lt_trans with (seq i).

eauto with schutte.
 auto.
 eauto with schutte.
 Qed.

 Hint Resolve mono_seq.
 Remark o_beta : ordinal beta.
 Proof.
  unfold beta.
  apply ordinal_omega_limit; auto with schutte.
 Qed.

 Remark alpha_lt_beta : alpha < beta.
 Proof.
  apply lt_trans with (seq 0).
  simpl.
  auto with schutte.
  unfold beta.
  apply lt_omega_limit;auto with schutte.
  intros; eapply lt_ordinal; eauto.
 Qed.


 Remark zero_lt_beta : zero < beta.
 apply le_lt_trans with alpha.
  eauto with schutte.
  apply alpha_lt_beta.
 Qed.

 Section ksi_fixed.
 Variable ksi: OT.
 Hypothesis o_ksi : ordinal ksi.
 Hypothesis lt_ksi : ksi < beta.

Remark lt_beta_exisys : exists n, ksi < seq n.
 unfold beta.
 intros.
 case (lt_omega_limit_lt_exists_lt ksi seq mono_seq); auto.
 intros;exists x;auto.
Qed.

Lemma inh_nat : nat.
 exact 0.
Qed.

Let n := epsilon inh_nat (fun n => ksi < seq n).

Remark ksi_plus_seq_n : forall (m:nat), (n <= m)%nat -> ksi + seq m <= beta.
 intros.
 apply le_trans with (seq (S m)).
 simpl.
 apply plus_mono_weak_l.
 eapply lt_ordinal.
 eapply mono_seq.
 apply le_trans with (seq n).
 right.
 pattern n; hilbert_e.
 apply lt_beta_exisys.
 elim H.
 left;split;auto with schutte.
 red;red;eapply lt_ordinal;eauto.
 intros; apply le_trans with (seq m0);auto.
 right;apply mono_seq.
 unfold beta.
 right;apply lt_omega_limit.
 intros; eapply lt_ordinal;eauto.
 red.
 apply seq_mono_intro.

 exact mono_seq.
Qed.

Lemma ksi_plus_seq_n' : forall (m:nat), ksi + seq m <= beta.
Proof.
 intros.
 case (le_or_lt n m).
 intros.
 apply ksi_plus_seq_n;auto.
 intros.
 apply le_trans with (ksi + seq n).
 apply plus_mono_r_weak;auto.
 eapply lt_ordinal;eauto.
 eapply lt_ordinal;eauto.
 assert (m <= n)%nat.
 auto with arith.
 right;fold lt.
 induction H.
 apply mono_seq.
 apply lt_trans with (seq m0);auto.
 apply IHle.
 auto with arith.
 pattern n;hilbert_e.
 apply lt_beta_exisys.
 intros.
 apply le_trans with (seq (S a)).
 simpl (seq (S a)).
 apply plus_mono_weak_l.
 eapply lt_ordinal;eauto.
 right;fold lt;apply H0.

 unfold beta.
 right; apply lt_omega_limit; auto with schutte.
 eauto with schutte.
Qed.

Lemma ksi_plus_beta : ksi + beta <= beta.
Proof.
 unfold beta at 1.
 unfold omega_limit.
 rewrite alpha_plus_sup.
 apply sup_least_upper_bound. eauto with schutte.
 apply R1 with ordinal (Greater ksi).
 apply plus_ordering; auto.
 apply seq_range_denumerable;auto.
  apply seq_mono_intro.

 exact mono_seq.

 red; destruct 1; eauto with schutte.

 destruct 1.
 decompose [and] H;subst y.
 apply ordinal_plus. eauto with schutte.
 case H0.
 intros; subst x.
 eauto with schutte.
 eauto with schutte.
destruct 1.
 decompose [and] H.
 subst y.
 decompose [and] H.
 case H1.
 intros;subst x.
 apply ksi_plus_seq_n'.
 eauto with schutte.
exists (seq 0).
 red.
 exists 0; trivial.
 eauto with schutte.

 red;destruct 1.
 subst x.
 red;eauto with schutte.
Qed.

Lemma ksi_plus_beta_eq : ksi + beta = beta.
apply le_antisym.
 apply ksi_plus_beta.
 apply le_plus_r;auto.
 apply o_beta.
Qed.

End ksi_fixed.

Lemma LLL : alpha < beta /\ AP beta.
Proof.
 split.
 apply alpha_lt_beta.
 split.
 apply zero_lt_beta.
 intros; apply ksi_plus_beta_eq; eauto with schutte.
Qed.

End AP_Unbounded.

Theorem AP_unbounded : Unbounded AP.
Proof.
 red.
 intros.
 generalize (LLL x H).
 exists (omega_limit
     (fix seq (n : nat) : M ON :=
        match n with
        | O => succ x
        | S p => seq p + seq p
        end)).
 tauto.
Qed.

Section AP_closed.
 Variable M : Ensemble OT.
 Hypothesis OM : Included M AP.
 Hypothesis inhM : Inhabited _ M.
 Hypothesis denM : denumerable M.

 Remark inc_M : Included M ordinal.
 Proof.
   red.
   intros.
   case (OM H);eauto with schutte.
 Qed.
 Remark supM_gt0 : zero < |_| M.
 Proof.
  case inhM.
  intros.
  apply lt_le_trans with x.
  case (OM H).
  auto.
  apply sup_upper_bound; auto with schutte.
  intros. generalize (OM H).
  destruct 1.
   generalize (OM H0).
  destruct 1;eauto with schutte.
 Qed.


 Lemma AP_sup : In AP (|_| M).
 Proof.
   red.
   split.
   apply supM_gt0.
   intros ksi Hksi.
   case (lt_sup_exists_lt denM inc_M ksi).
   eauto with schutte.
 auto.
  intros alpha (Malpha, ksialpha).
  apply le_antisym.
  2:apply le_plus_r;eauto with schutte.


  rewrite alpha_plus_sup.
  2:eauto with schutte.

  apply sup_mono.
  apply R1 with ordinal (Greater ksi).
  apply plus_ordering; eauto with schutte.
  auto.
  red. intros.
  case (OM H); eauto with schutte.
  auto.
  red;destruct 1.
  decompose [and] H;subst x.
  red;apply ordinal_plus;auto with schutte.
  eauto with schutte.

 case (OM H0);eauto with schutte.
 apply inc_M.

  intros.
    case H.
  intros beta (Mbeta,ebeta).
  case (lt_or_ge beta alpha);auto with schutte.

   apply inc_M.
   auto.
 eauto with schutte.

exists alpha.
   split;auto.
  subst x.
  case (OM Mbeta).
 intros.
  right.
 fold lt.

  apply lt_le_trans with (ksi + alpha).
  apply plus_mono_r; eauto with schutte.
  left.
  split;auto.
 red.
 fold ordinal.
 eapply ordinal_plus;eauto with schutte.
 case (OM Malpha).
 intros.
  auto.

  exists beta.
  split.
  auto.
  left.
 split.
 subst x;red;apply ordinal_plus;eauto with schutte.
 subst x.
  case (OM Mbeta).
  intros.
 apply H2.
 apply lt_le_trans with alpha;auto.
  auto.
 auto.
 apply inc_M.
Qed.


End AP_closed.

Theorem AP_closed : closed AP.
 split.
 red; destruct 1 ;eauto with schutte.
 intros.
 apply AP_sup;auto.
Qed.







Definition phi0 := the_ordering_function AP.

Lemma AP_Inc_ordinal : Included AP ordinal.
Proof.
 red; destruct 1; eauto with schutte.
Qed.

Lemma AP_o_segment : the_ordering_segment AP = ordinal.
Proof.
 intros;apply O_segment_unbounded.
 eapply SA2.
 eapply the_ordering_function_ok;eauto.
 apply AP_Inc_ordinal.
 generalize
   (ordering_unbounded_unbounded
     (A:=the_ordering_segment AP)
     (B:=AP)
     (f:=phi0)).

intros.
 generalize (H (AP_Inc_ordinal)).
 intro; clear H.
 unfold phi0.
 generalize (H0 (the_ordering_function_ok AP_Inc_ordinal )).
 destruct 1.
 apply H.
 apply AP_unbounded;auto.
Qed.

Theorem normal_phi0 : normal phi0 AP.
 apply TH_13_6R with ordinal.
 red;destruct 1;red;eauto with schutte.
 unfold phi0.

 pattern (the_ordering_function AP).

 hilbert_e.
 exists (the_ordering_function AP).
 apply the_ordering_function_ok.
 apply AP_Inc_ordinal.
 intros.
 rewrite AP_o_segment in H.
 auto.
apply AP_closed.
 apply AP_unbounded.
Qed.


Lemma phi0_ordering : ordering_function phi0 ordinal AP.
Proof.
  intros.
  unfold phi0.
  pattern (the_ordering_function AP); epsilon_elim.
 exists (the_ordering_function AP).
 apply the_ordering_function_ok.
 apply AP_Inc_ordinal.
  rewrite <- (AP_o_segment);auto.
Qed.

Lemma phi0_elim : forall P : (OT->OT)->Prop,
                     (forall f: OT->OT,
                       ordering_function f ordinal AP-> P f) ->
                      P phi0.
Proof.
 intros.
 apply H.
 apply phi0_ordering.
Qed.

  Lemma AP_phi0 : forall alpha, ordinal alpha -> AP (phi0 alpha).
  intros; pattern phi0; apply phi0_elim.
  destruct 1.
  decompose [and] H1.
 apply H4;auto.
 Qed.


Lemma ordinal_phi0 : forall alpha, ordinal alpha -> ordinal (phi0 alpha).
Proof.
 intros.
 pattern (phi0 alpha).
 apply phi0_elim; auto with schutte.
 intros.
  eapply ordering_function_ordinal_B;eauto.
Qed.

Hint Resolve ordinal_phi0: schutte.

Lemma phi0_zero : phi0 zero = F 1.
  generalize (order_function_least_least phi0_ordering).
  generalize least_AP.
  intros.

  rewrite (least_member_unicity ON H H0);eauto.
Qed.

Lemma phi0_mono : forall alpha beta, alpha < beta ->
                                     phi0 alpha < phi0 beta.
intros.
pattern phi0.
apply phi0_elim.
intros;eapply ordering_function_mono;eauto with schutte.
Qed.

 Lemma phi0_mono_weak : forall alpha beta, alpha <= beta ->
                                           phi0 alpha <= phi0 beta.
 Proof.
   destruct 1.
   decompose [and] H.
    subst beta; auto with schutte.
    right;apply phi0_mono;auto.
 Qed.

Lemma phi0_mono_R : forall alpha beta, ordinal alpha -> ordinal beta ->
                          phi0 alpha < phi0 beta -> alpha < beta.
Proof.
 intros alpha beta Oalpha Obeta.
 pattern phi0.
apply phi0_elim.
 intros;eapply ordering_function_monoR; eauto;ordi.
Qed.

Lemma phi0_mono_R_weak : forall alpha beta, ordinal alpha -> ordinal beta ->
                          phi0 alpha <= phi0 beta -> alpha <= beta.
Proof.
 intros alpha beta Oalpha Obeta.
 pattern phi0.
apply phi0_elim.
 intros.
 eapply ordering_function_mono_weakR;eauto;ordi.
Qed.

Lemma phi0_inj : forall alpha beta, ordinal alpha -> ordinal beta ->
                            phi0 alpha = phi0 beta ->alpha = beta.
Proof.
 intros; apply le_antisym; apply phi0_mono_R_weak;auto;ordi;
 auto with schutte.
Qed.

Lemma phi0_positive : forall alpha, ordinal alpha -> zero < phi0 alpha.
Proof.
  intros.
  apply lt_le_trans with (phi0 zero).
  rewrite phi0_zero.
  eauto with schutte arith.

  pattern phi0 ; apply phi0_elim.
  intros.
  eapply ordering_function_mono_weak; eauto with schutte.
Qed.

Lemma plus_lt_phi0 : forall ksi alpha, ordinal alpha ->
                                       ksi < phi0 alpha ->
                                       ksi + phi0 alpha = phi0 alpha.
Proof.
 intros ksi alpha Halpha.
 pattern (phi0 alpha).
 apply phi0_elim.
 intros f Hf.
 assert (AP (f alpha)).

 case Hf.
 intros.
 decompose [and] H0; clear H0.
 apply H3.
 red;auto.
 case H.
 auto.
Qed.

Lemma phi0_alpha_phi0_beta : forall alpha beta, alpha < beta ->
                                                 phi0 alpha + phi0 beta =
                                                 phi0 beta.
Proof.
 intros.
 apply plus_lt_phi0; eauto with schutte.
 apply phi0_mono.
 auto.
Qed.

Lemma phi0_sup : forall U, Included U ordinal -> Inhabited _ U ->
                           denumerable U ->
                           phi0 (sup U) = sup (image U phi0).
Proof.
 intros.
 case normal_phi0.
 destruct 2;symmetry; auto.
Qed.

Lemma phi0_of_limit : forall alpha, is_limit alpha ->
                                    phi0 alpha =
                                    sup (image (members alpha) phi0).
Proof.
  intros.
  pattern alpha at 1;
   rewrite (is_limit_sup_members H).
   case normal_phi0.
 destruct 2;symmetry;auto.
 apply H3.
 red;destruct 1;auto.
 exists zero.
 red.
 red.
 split.
 red;auto with schutte.
 red.
 case H;auto.
 destruct 2.
 tricho zero alpha HH.
 auto.
 subst alpha; case (H5);auto.
 case (not_lt_zero alpha);auto.
 apply denumerable_members;auto.
 case H;auto.
Qed.

Lemma AP_to_phi0 : forall alpha, AP alpha -> exists beta, ordinal beta /\
                                                          alpha = phi0 beta.
 intros.
 pattern phi0;apply phi0_elim.
 destruct 1.
 decompose [and] H1.
 case (H3 _ H).
 intro x;exists x.
 split;auto.
 case H5;auto.
 case H5;auto.
Qed.

Definition log (alpha : OT) := sup (fun beta => ordinal beta /\
                                                 phi0 beta <= alpha).

Lemma log_ordinal : forall alpha, zero < alpha -> ordinal (log alpha).
 unfold log.
 intros.
 apply sup_ordinal.
 apply AX2.
 red.
 destruct 1.
 red;auto.
 exists (succ alpha).
 split;ordi.
 destruct 1.
 apply le_lt_trans with (phi0 y);auto.
 pattern phi0;apply phi0_elim.
 intros;
 eapply ordering_le;eauto.
  apply le_lt_trans with alpha;auto.
 eauto with schutte.
 tauto.
 Qed.



Lemma phi0_log_le : forall alpha, zero < alpha ->
                       phi0 (log alpha) <= alpha.
Proof.
 intros; unfold log.
 rewrite phi0_sup.
apply sup_least_upper_bound.
 apply R1 with ordinal AP.
 apply phi0_ordering.
 apply AX2.
 red.
 destruct 1.
 red;auto.

 exists (succ alpha).
 split;ordi.
 destruct 1.
apply le_lt_trans with (phi0 y);auto.
 pattern phi0;apply phi0_elim.
 intros;
 eapply ordering_le;eauto.
  apply le_lt_trans with alpha;auto.
 eauto with schutte.
 red; destruct 1; eauto with schutte.
 red.
 destruct 1.
 case H0.
 destruct 1.
 fold ordinal.
 intro;subst y;ordi.
 ordi.
 destruct 1.
 decompose [and] H0.
 red in H1.
 decompose [and] H1.
 subst y;auto.
 red.
 destruct 1.
 red;auto.
 exists zero.
 red.
 split.
 auto with schutte.
 rewrite phi0_zero.
 simpl;apply lt_succ_le.
 ordi.
 ordi.
 auto.
 apply AX2.
 red;destruct 1.
 red.
 auto.
 exists (succ alpha).
 split;ordi.
 destruct 1.
 apply le_lt_trans with (phi0 y);auto.
 pattern phi0;apply phi0_elim.
 intros;
 eapply ordering_le;eauto.
  apply le_lt_trans with alpha;auto.
 eauto with schutte.
Qed.

Lemma AP_plus_AP : forall alpha beta gamma, ordinal alpha ->
                   zero < beta -> ordinal gamma ->
                    phi0 alpha + beta = phi0 gamma -> alpha < gamma /\
                            beta = phi0 gamma.
Proof.
 intros.
 tricho alpha gamma H3.
 split;auto.
 tricho beta (phi0 gamma) H4.
 auto.
 ordi.
 case (lt_irr (phi0 gamma)).
 pattern (phi0 gamma) at 1.
 rewrite <- H2.
 apply AP_plus_closed.
 apply AP_phi0;
 eauto with schutte.
 apply phi0_mono;auto.
 auto.
 auto.
 rewrite <- H2 in H4.
 case (lt_irr beta).
 eapply le_lt_trans;eauto.
 apply le_plus_r.
 ordi.
 ordi.
 subst gamma.
 case (lt_irr (phi0 alpha)).
 pattern (phi0 alpha) at 2.
 rewrite <- H2.
 pattern (phi0 alpha) at 1; rewrite <- alpha_plus_zero.
 apply plus_mono_r;auto.
 ordi.
 ordi.
 assert( phi0 alpha <= phi0 gamma).
 rewrite <- H2.
 apply le_plus_l.
 ordi.
 ordi.
 case (le_not_gt H4).
 apply phi0_mono;auto.
Qed.

Lemma is_limit_phi0 : forall alpha, zero < alpha ->
                                    is_limit (phi0 alpha).
Proof.
 intros.
 split.
 ordi.
 split.
 red.
 intros.
 case (lt_irr zero).
 apply lt_le_trans with alpha;auto.
 rewrite <- H0.

 pattern phi0; apply phi0_elim.

 intros.
 eapply ordering_le;eauto.
 ordi.

  red.
 destruct 1.

 decompose [and] H0.
 generalize (AP_phi0 alpha).
 intro.
 case H3.
 ordi.
 intros.

 rewrite H2 in H5.
 assert (x < succ x).
 auto with schutte.
 generalize (H5 _ H6).
 rewrite plus_of_succ; auto.
 intros.

 assert (zero < x).
 tricho zero x H8.
 auto.
 subst x.
 replace (succ zero) with (F 1) in H2.
 rewrite <- phi0_zero in H2.
 case (lt_irr (phi0 zero)).
 pattern (phi0 zero) at 2; rewrite <- H2.
 apply phi0_mono;auto.
 simpl;auto.
 case (not_lt_zero x).
 auto.
 assert (x < x+x).
 pattern x at 1;rewrite <- alpha_plus_zero.

 apply plus_mono_r;auto.
 auto.
 assert (ordinal (x+x)).
 ordi.

 generalize (succ_mono H1 H10 H9).
 rewrite <- H7.
 intros; apply lt_irr with (succ (x+x)).
 auto.
Qed.