From Coq Require Import Arith Max Bool Lia Compare_dec Relations Ensembles
     Wellfounded Bool RelationClasses Operators_Properties ArithRing
     Logic.Eqdep_dec.

From Coq Require PArith.
From hydras Require Import More_Arith Restriction DecPreOrder.
From hydras Require Import OrdNotations.
From hydras Require Export Prelude.Comparable.
From hydras Require Export STDPP_compat.

Create HintDb T1.

Set Implicit Arguments.

Declare Scope t1_scope.
Delimit Scope t1_scope with t1.
Open Scope t1_scope.

Coercion is_true: bool >-> Sortclass.

Inductive T1 : Set :=
| zero
| cons (alpha : T1) (n : nat) (beta : T1) .

Notation FS n := (cons zero n zero).

Notation one := (FS 0).

Definition T1nat (n:nat) := match n with 0 ⇒ zero | S p ⇒ FS p end.

Notation "\F n" := (T1nat n) (at level 29): t1_scope.

Coercion T1nat : nat >-> T1.

Example ten : T1 := 10.

#[deprecated(note="use T1nat" )]
 Notation fin := T1nat (only parsing).


Notation T1omega := (cons (cons zero 0 zero) 0 zero).


#[deprecated(note="use T1omega")]
 Notation omega := T1omega (only parsing).

Fixpoint T1is_succ alpha :=
  match alpha with
    | zero ⇒ false
    | cons zero _ _ ⇒ true
    | cons _alpha _n beta ⇒ T1is_succ beta
  end.

Fixpoint T1limit alpha :=
  match alpha with
    | zero ⇒ false
    | cons zero _ _ ⇒ false
    | cons _ _ zero ⇒ true
    | cons _ _ beta ⇒ T1limit beta
  end.





#[deprecated(note="use T1is_succ")]
  Notation succb := T1is_succ (only parsing).

#[deprecated(note="use T1limit")]
  Notation limitb := T1limit (only parsing).

Notation phi0 alpha := (cons alpha 0 zero).

Definition omega_term (alpha:T1)(k:nat) :=
  cons alpha k zero.

Fixpoint omega_tower (height:nat) : T1 :=
  match height with
  | 0 ⇒ one
  | S h ⇒ phi0 (omega_tower h)
  end.

Inductive ap : T1 → Prop :=
  ap_intro : ∀ a, ap (phi0 a).

#[global] Instance compare_T1 : Compare T1 :=
 fix cmp (alpha beta:T1) :=
  match alpha, beta with
  | zero, zero ⇒ Eq
  | zero, cons a' n' b' ⇒ Lt
  | _ , zero ⇒ Gt
  | (cons a n b),(cons a' n' b') ⇒
      (match cmp a a' with
       | Lt ⇒ Lt
       | Gt ⇒ Gt
       | Eq ⇒ (match n ?= n' with
                | Eq ⇒ cmp b b'
                | comp ⇒ comp
                end)
       end)
  end.

Definition lt (alpha beta : T1) : Prop :=
  compare alpha beta = Lt.

Notation le := (leq lt).

Example E1 : lt (cons T1omega 56 zero) (omega_tower 3).

Example E2 : ¬ lt (omega_tower 3) (cons T1omega 5 (omega_tower 3))%t1.

Lemma compare_cons :
 ∀ a n b a' n' b',
 compare (cons a n b) (cons a' n' b') =
 match compare a a' with
 | Lt ⇒ Lt
 | Gt ⇒ Gt
 | Eq ⇒ (match n ?= n' with
        | Eq ⇒ compare b b'
        | comp ⇒ comp
        end)
 end.


Lemma compare_rev :
  ∀ (alpha beta : T1),
  compare beta alpha = CompOpp (compare alpha beta).
Lemma compare_reflect :
  ∀ alpha beta,
    match compare alpha beta with
    | Lt ⇒ lt alpha beta
    | Eq ⇒ alpha = beta
    | Gt ⇒ lt beta alpha
    end.

Lemma compare_correct (alpha beta: T1):
  CompSpec eq lt alpha beta (compare alpha beta).

Lemma compare_refl :
  ∀ alpha : T1, compare alpha alpha = Eq.

Lemma compare_eq_iff (a b : T1) :
  compare a b = Eq ↔ a = b.

Theorem not_lt_zero alpha : ¬ lt alpha zero.

#[global] Hint Resolve not_lt_zero : T1.

Lemma compare_lt_impl a b :
  compare a b = Lt → lt a b.

Lemma compare_lt_iff a b :
  compare a b = Lt ↔ lt a b.

Inductive lt_cases (a b : T1) (n :nat) (a' b':T1) (n':nat) : Type :=
  | lt_left (H : lt a a')
  | lt_middle (H : a = a')(H1 : (n < n')%nat)
  | lt_right (H : a = a')(H1 : n = n')(H2 : lt b b').

Lemma lt_inv_strong :
  ∀ a n b a' n' b',
  lt (cons a n b) (cons a' n' b') →
  lt_cases a b n a' b' n'.

Theorem lt_irrefl (alpha: T1):
  ¬ lt alpha alpha.

Theorem lt_inv :
  ∀ a n b a' n' b',
  lt (cons a n b) (cons a' n' b') →
  lt a a' ∨
  a = a' ∧ (n < n')%nat ∨
  a = a' ∧ n = n' ∧ lt b b'.

Lemma lt_inv_coeff:
  ∀ a n n' b b',
  lt (cons a n b) (cons a n' b') → n ≤ n'.

Lemma lt_inv_coeff_dec :
  ∀ a n n' b b',
  lt (cons a n b) (cons a n' b') →
  {(n < n')%nat} + { n = n' ∧ lt b b'}.

Lemma lt_inv_tail :
  ∀ a n b b',
  lt (cons a n b) (cons a n b') → lt b b'.

Lemma head_lt :
  ∀ alpha alpha' n n' beta beta',
       lt alpha alpha' →
       lt (cons alpha n beta) (cons alpha' n' beta').

Lemma coeff_lt :
  ∀ alpha n n' beta beta',
  (n < n')%nat → lt (cons alpha n beta) (cons alpha n' beta').

Lemma tail_lt :
  ∀ alpha n beta beta',
  lt beta beta' →
  lt (cons alpha n beta) (cons alpha n beta').

Lemma compare_fin_rw (n n1: nat) :
  compare (T1nat n) (T1nat n1) = (n ?= n1).

Lemma lt_fin_iff (i j : nat): lt (T1nat i) (T1nat j) ↔ Nat.lt i j.

Theorem lt_trans:
  ∀ alpha beta gamma: T1,
  lt alpha beta → lt beta gamma → lt alpha gamma.


#[global] Instance t1_strorder: StrictOrder lt.
#[global] Instance: Comparable lt compare.

Lemma lt_inv_head :
  ∀ a n b a' n' b',
    lt (cons a n b) (cons a' n' b') → leq lt a a'.

#[ global ] Instance lt_dec : RelDecision lt :=
fun alpha beta ⇒ decide (compare alpha beta = Lt).

Fixpoint nf_b (alpha : T1) : bool :=
  match alpha with
  | zero ⇒ true
  | cons a n zero ⇒ nf_b a
  | cons a n ((cons a' n' b') as b) ⇒
      (nf_b a && nf_b b && (bool_decide (lt a' a)))%bool
  end.

Definition nf alpha :Prop := nf_b alpha.


Example bad_term: T1 := cons 1 1 (cons T1omega 2 zero).

Definition epsilon_0 : Ensemble T1 := nf.

Fixpoint succ (a: T1) : T1 :=
  match a with
  | zero ⇒ T1nat 1
  | cons zero n _ ⇒ cons zero (S n) zero
  | cons b n c ⇒ cons b n (succ c)
  end.

Fixpoint pred (c:T1) : option T1 :=
  match c with zero ⇒ None
  | cons zero 0 _ ⇒ Some zero
  | cons zero (S n) _ ⇒ Some (cons zero n zero)
  | cons a n b ⇒
      match (pred b) with
      | None ⇒ None
      | Some c ⇒ Some (cons a n c)
      end
  end.

Fixpoint T1add (a b : T1) :T1 :=
  match a, b with
  | zero, y ⇒ y
  | x, zero ⇒ x
  | cons a n b, cons a' n' b' ⇒
      (match compare a a' with
       | Lt ⇒ cons a' n' b'
       | Gt ⇒ (cons a n (T1add b (cons a' n' b')))
       | Eq ⇒ (cons a (S (n+n')) b')
       end)
  end
where "alpha + beta" := (T1add alpha beta) : t1_scope.

#[deprecated(note="use T1add")]
  Notation plus := T1add (only parsing).

Fixpoint T1mul (a b : T1) :T1 :=
  match a, b with
  | zero, _ ⇒ zero
  | _, zero ⇒ zero
  | cons zero n _, cons zero n' b' ⇒
      cons zero (Peano.pred((S n) × (S n'))) b'
  | cons a n b, cons zero n' _ ⇒
      cons a (Peano.pred ((S n) × (S n'))) b
  | cons a n b, cons a' n' b' ⇒
      cons (a + a') n' ((cons a n b) × b')
  end
where "a * b" := (T1mul a b) : t1_scope.

#[deprecated(note="use T1mul")]
  Notation mult := T1mul (only parsing).

Fixpoint minus (alpha beta : T1) :T1 :=
  match alpha,beta with
 | zero, y ⇒ zero
 | cons zero n _, cons zero n' _ ⇒
     if (le_lt_dec n n')
     then zero
     else cons zero (Peano.pred (n-n')) zero
 | cons zero n _, zero ⇒ cons zero n zero
 | cons zero _ _, _ ⇒ zero
 | cons a n b, zero ⇒ cons a n b
 | cons a n b, cons a' n' b' ⇒
     (match compare a a' with
      | Lt ⇒ zero
      | Gt ⇒ cons a n b
      | Eq ⇒ (match Nat.compare n n' with
               | Lt ⇒ zero
               | Gt ⇒ (cons a (Peano.pred (n - n')) b')
               | Eq ⇒ b - b'
               end)
       end)
 end
 where "alpha - beta" := (minus alpha beta):t1_scope.

Fixpoint exp_F (alpha : T1)(n : nat) :T1 :=
 match n with
 | 0 ⇒ FS 0
 | S p ⇒ alpha × (exp_F alpha p)
 end.

Fixpoint exp (alpha beta : T1) :T1 :=
  match alpha ,beta with
 | _, zero ⇒ cons zero 0 zero
 | cons zero 0 _ , _ ⇒ cons zero 0 zero
 | zero, _ ⇒ zero
 | x , cons zero n' _ ⇒ exp_F x (S n')
 | cons zero n _, cons (cons zero 0 zero) n' b' ⇒
        ((cons (cons zero n' zero) 0 zero) ×
                ((cons zero n zero) ^ b'))
 | cons zero n _, cons a' n' b' ⇒
            (omega_term
                    (omega_term (a' - 1) n')
                    0) ×
                 ((cons zero n zero) ^ b')
 | cons a n b, cons a' n' b' ⇒
    ((omega_term (a × (cons a' n' zero))
                            0) ×
            ((cons a n b) ^ b'))
end
where "alpha ^ beta " := (exp alpha beta) : t1_scope.

Lemma compare_of_phi0 alpha beta:
  compare (phi0 alpha) (phi0 beta) = compare alpha beta.

Lemma zero_lt : ∀ alpha n beta, lt zero (cons alpha n beta).

#[global] Hint Resolve zero_lt head_lt coeff_lt tail_lt : T1.

Open Scope t1_scope.

Lemma zero_nf : nf zero.

Lemma single_nf :
  ∀ a n, nf a → nf (cons a n zero).

Lemma cons_nf :
  ∀ a n a' n' b,
  lt a' a →
  nf a →
  nf(cons a' n' b)→
  nf(cons a n (cons a' n' b)).

#[global] Hint Resolve zero_nf single_nf cons_nf: T1.

Lemma nf_inv1 :
  ∀ a n b, nf (cons a n b) → nf a.

Lemma nf_inv2 :
  ∀ a n b, nf (cons a n b) → nf b.

Lemma nf_inv3 :
  ∀ a n a' n' b',
  nf (cons a n (cons a' n' b')) → lt a' a.

Lemma nf_cons_inv a n b : nf (cons a n b) → nf a ∧ nf b ∧ lt b (phi0 a).

Lemma nf_cons_iff a n b : nf (cons a n b) ↔ nf a ∧ nf b ∧ lt b (phi0 a).

Lemma bool_eq_iff (b b':bool) : (b = b') ↔ (b ↔ b').

Lemma nf_b_cons_eq a n b : nf_b (cons a n b) =
                           nf_b a && nf_b b && bool_decide (lt b (phi0 a)).


Ltac nf_decomp H :=
  let nf0 := fresh "nf"
  in let nf1 := fresh "nf"
     in let Hlp := fresh "lt"
     in
     match type of H with
     | nf (cons ?t ?n zero) ⇒ assert (nf0:= nf_inv1 H)
     | nf (cons ?t1 ?n (cons ?t2 ?p ?t3))
       ⇒ assert (nf0 := nf_inv1 H); assert(nf1 := nf_inv2 H);
          assert (lt := nf_inv3 H)
     | nf (cons ?t1 ?n ?t2) ⇒ assert (nf0 := nf_inv1 H); assert(nf1 := nf_inv2 H)
     end.

Inductive lt_a_phi0_b : T1 → T1 → Prop :=
| lt_a_phi0_b_z : ∀ alpha, lt_a_phi0_b zero alpha
| lt_a_phi0_b_c : ∀ alpha alpha' n' beta',
                  lt alpha' alpha →
                  lt_a_phi0_b (cons alpha' n' beta') alpha.

#[global] Hint Constructors lt_a_phi0_b : T1.

Reserved Notation "x '<_phi0' y" (at level 70, no associativity).
Infix "<_phi0" := lt_a_phi0_b.


Definition get_decomposition : ∀ c:T1, lt zero c →
                           {a:T1 & {n:nat & {b:T1 | c = cons a n b}}}.

Ltac decomp_exhib H a n b e:=
 let Ha := fresh in
 let Hn := fresh in
 let Hb := fresh in
  match type of H
  with lt zero ?c ⇒
    case (get_decomposition H);
     intros a Ha;
     case Ha;intros n Hn; case Hn; intros b e;
     clear Ha Hn
  end.

Lemma nf_FS : ∀ n:nat, nf (FS n).

Lemma nf_fin : ∀ n:nat, nf (T1nat n).

Lemma succ_not_zero : ∀ alpha, succ alpha ≠ zero.

Lemma succ_is_succ : ∀ alpha, T1is_succ (succ alpha).

Lemma finite_lt :
  ∀ n p : nat, (n < p)%nat → lt (FS n) (FS p).

Lemma finite_ltR :
  ∀ n p : nat,
  lt (FS n) (FS p) → (n < p)%nat.

Lemma le_eq_lt_dec alpha beta:
  leq lt alpha beta →
  {alpha = beta} + {lt alpha beta}.

Lemma lt_succ (alpha : T1) : lt alpha (succ alpha).

Lemma lt_a_phi0_a :
  ∀ a, lt a (phi0 a).

Lemma phi0_lt :
  ∀ a b, lt a b → lt (phi0 a) (phi0 b).

Lemma phi0_ltR :
  ∀ a b, lt (phi0 a) (phi0 b) → lt a b.

Lemma nf_of_finite :
  ∀ n b,
  nf (cons zero n b) → b = zero.

Theorem zero_le :
  ∀ a, leq lt zero a.

Theorem le_inv :
  ∀ a n b a' n' b',
  leq lt (cons a n b) (cons a' n' b') →
  lt a a' ∨
  a = a' ∧ (n < n')%nat ∨
  a = a' ∧ n = n' ∧ leq lt b b'.

Arguments le_inv [a n b a' n' b'] _.

Lemma lt_a_phi0_b_inv :
  ∀ a n b a', lt (cons a n b) (phi0 a') → lt a a'.

Theorem le_zero_inv :
  ∀ a, leq lt a zero → a = zero.

Theorem le_tail :
  ∀ a n b b',
  leq lt b b' →
  leq lt (cons a n b) (cons a n b').

#[global] Hint Resolve zero_le le_tail : T1.

Theorem le_phi0 :
  ∀ a n b, leq lt (phi0 a) (cons a n b).

Lemma head_lt_cons :
  ∀ a n b, lt a (cons a n b).

#[export] Hint Resolve head_lt_cons: T1.

Definition T1_eq_dec (alpha beta : T1):
{alpha = beta} + {alpha ≠ beta}.

Definition lt_eq_lt_dec :
  ∀ alpha beta : T1,
  {lt alpha beta} + {alpha = beta} + {lt beta alpha}.

Definition lt_le_dec (alpha beta : T1) :
  {lt alpha beta} + {leq lt beta alpha}.

#[ global ] Instance epsilon0_pre_order : TotalPreOrder (leq lt).

#[ global ] Instance epsilon0_dec : RelDecision (leq lt).

Ltac auto_nf :=
  match goal with
    |- nf ?alpha ⇒
    ( repeat (apply cons_nf || apply single_nf || apply zero_nf))
    || (eapply nf_inv1 || eapply nf_inv2); eauto
  end.

Lemma nf_tail_lt_nf b b':
  lt b' b → nf b' →
  ∀ a n, nf (cons a n b) → nf (cons a n b').

Lemma tail_lt_cons :
  ∀ b n a,
  nf (cons a n b) → lt b (cons a n b).

Lemma lt_a_phi0_b_inv1 :
  ∀ a n b a', cons a n b <_phi0 a'→ lt a a'.

Lemma nf_intro :
  ∀ a n b, nf a → nf b → b <_phi0 a →
                nf (cons a n b).

Lemma nf_intro' :
  ∀ a n b,
  nf a →
  nf b →
  lt b (cons a 0 zero) →
  nf (cons a n b).

Lemma lt_a_phi0_b_intro :
  ∀ a n b, nf (cons a n b) → b <_phi0 a.

Lemma nf_coeff_irrelevance :
  ∀ a b n p, nf (cons a n b) → nf (cons a p b).

Lemma lt_a_phi0_b_phi0 :
  ∀ a b, b <_phi0 a → lt b ( phi0 a).

Lemma lt_a_phi0_b_phi0R :
  ∀ a b, lt b (phi0 a) → b <_phi0 a.

Lemma lt_a_phi0_b_def :
  ∀ a b, b <_phi0 a ↔ lt b (phi0 a).

Lemma lt_a_phi0_b_iff :
  ∀ a b, nf a → nf b →
              (b <_phi0 a ↔ ∀ n, nf (cons a n b)).

Lemma nf_omega_tower : ∀ n, nf (omega_tower n).

Definition nf_rect : ∀ P : T1 → Type,
    P zero →
    (∀ n: nat, P (cons zero n zero)) →
    (∀ a n b n' b', nf (cons a n b) →
                         P (cons a n b)→
                         lt b' (phi0 (cons a n b)) →
                         nf b' →
                         P b' →
                         P (cons (cons a n b) n' b')) →
    ∀ a: T1, nf a → P a.

Theorem compare_reflectR ( alpha beta : T1) :
  (match lt_eq_lt_dec alpha beta with
   | inleft (left _) ⇒ Lt
   | inleft (right _) ⇒ Eq
   | inright _ ⇒ Gt
   end)
  = compare alpha beta.

Lemma max_nf (alpha beta : T1) :
  nf alpha → nf beta → nf (max alpha beta).

Reserved Notation "x 't1<' y" (at level 70, no associativity).
Reserved Notation "x 't1<=' y" (at level 70, no associativity).
Reserved Notation "x 't1>=' y" (at level 70, no associativity).
Reserved Notation "x 't1>' y" (at level 70, no associativity).

Reserved Notation "x 't1<=' y 't1<=' z" (at level 70, y at next level).
Reserved Notation "x 't1<=' y 't1<' z" (at level 70, y at next level).
Reserved Notation "x 't1<' y 't1<' z" (at level 70, y at next level).
Reserved Notation "x 't1<' y 't1<=' z" (at level 70, y at next level).


Definition LT := restrict nf lt.
Infix "t1<" := LT : t1_scope.

Definition LE := restrict nf (leq lt).
Infix "t1<=" := LE : t1_scope.


Notation "alpha t1< beta t1< gamma" :=
  (LT alpha beta ∧ LT beta gamma) : t1_scope.

Definition Elements alpha : Ensemble T1 :=
  fun beta ⇒ beta t1< alpha.

Coercion Elements : T1 >-> Ensemble.

Lemma LT_nf_l : ∀ alpha beta , alpha t1< beta → nf alpha.

Lemma LT_nf_r : ∀ alpha beta , alpha t1< beta → nf beta.

Lemma LT_lt alpha beta : alpha t1< beta → lt alpha beta.

Lemma LE_nf_l : ∀ alpha beta , alpha t1≤ beta → nf alpha.

Lemma LE_nf_r : ∀ alpha beta , alpha t1≤ beta → nf beta.

Lemma LE_le alpha beta : alpha t1≤ beta → leq lt alpha beta.

#[global] Hint Resolve LT_nf_r LT_nf_l LT_lt LE_nf_r LE_nf_l LE_le : T1.

Lemma not_zero_gt_0 (alpha:T1) : alpha ≠ zero → lt zero alpha.

Lemma not_zero_lt (alpha: T1): nf alpha → alpha ≠ zero →
                               zero t1< alpha.

Lemma LE_zero : ∀ alpha, nf alpha → zero t1≤ alpha.

Lemma LE_refl : ∀ alpha, nf alpha → alpha t1≤ alpha.

Lemma LT_trans : ∀ a b c:T1, a t1< b → b t1< c → a t1< c.

Theorem LE_trans (alpha beta gamma: T1):
          alpha t1≤ beta → beta t1≤ gamma → alpha t1≤ gamma.

Lemma LE_antisym (alpha beta : T1): alpha t1≤ beta →
                                     beta t1≤ alpha →
                                     alpha = beta.

Lemma LT1 : ∀ alpha n beta, nf (cons alpha n beta) →
                                 zero t1< cons alpha n beta.

Lemma LT2 : ∀ alpha alpha' n n' beta beta',
    nf (cons alpha n beta) →
    nf (cons alpha' n' beta') →
    alpha t1< alpha' →
    cons alpha n beta t1< cons alpha' n' beta'.

Lemma LT3 : ∀ alpha n n' beta beta',
    nf (cons alpha n beta) →
    nf (cons alpha n' beta') →
    n < n' →
    cons alpha n beta t1< cons alpha n' beta'.

Lemma LT4 : ∀ alpha n beta beta',
    nf (cons alpha n beta) →
    nf (cons alpha n beta') →
    beta t1< beta' →
    cons alpha n beta t1< cons alpha n beta'.

#[global] Hint Resolve LT1 LT2 LT3 LT4: T1.

Lemma LT_irrefl (alpha : T1) :
  ¬ alpha t1< alpha.

Lemma LE_LT_trans :
  ∀ alpha beta gamma,
  alpha t1≤ beta → beta t1< gamma → alpha t1< gamma.

Lemma LT_LE_trans (alpha beta gamma : T1) : alpha t1< beta →
                                            beta t1≤ gamma →
                                            alpha t1< gamma.

Lemma not_LT_zero :
  ∀ alpha, ¬ alpha t1< zero.

#[ global ] Instance LT_St : StrictOrder LT.

Lemma nf_cons_LT :
  ∀ (a : T1) (n : nat) (a' : T1) (n' : nat) (b : T1),
  a' t1< a →
  nf a → nf (cons a' n' b) → nf (cons a n (cons a' n' b)).

#[global] Hint Resolve nf_cons_LT: T1.

#[global] Hint Resolve nf_inv1 nf_inv2 nf_inv3 : T1.

Lemma head_LT_cons :
  ∀ alpha n beta,
  nf (cons alpha n beta) →
  alpha t1< cons alpha n beta.

Lemma tail_LT_cons :
  ∀ alpha n beta,
  nf (cons alpha n beta) →
  beta t1< cons alpha n beta.

Lemma LT_inv : ∀ a n b a' n' b',
    cons a n b t1< cons a' n' b' →
    a t1< a' ∨
    a = a' ∧ (n < n' ∨ n = n' ∧ b t1< b').

Inductive LT_cases (a b : T1) (n :nat) (a' b':T1) (n':nat) : Type :=
| LT_left (H : a t1< a')
| LT_middle (H : a = a')(H1 : n < n')
| LT_right (H : a = a')(H1 : n = n')(H2 : b t1< b').

Lemma LT_inv_strong :
  ∀ a b n a' b' n',
  cons a n b t1< cons a' n' b' → LT_cases a b n a' b' n'.

Lemma remove_first_sumand :
  ∀ a n b b',
    cons a n b t1< cons a n b' → b t1< b'.

Lemma LT_cons_0 :
  ∀ a n b a' b',
  cons a n b t1< cons a' 0 b' → a t1< a' ∨ n = 0 ∧ a = a' ∧ b t1< b'.

Lemma LE_phi0 :
  ∀ a n b, nf (cons a n b) → phi0 a t1≤ cons a n b.

Lemma nf_tail_lt alpha n beta gamma :
  nf (cons alpha n beta) → gamma t1< beta →
  nf (cons alpha n gamma).

Module Direct_proof.
  Section well_foundedness_proof.
    #[local] Hint Unfold restrict LT: T1.

    Lemma Acc_zero : Acc LT zero.



    Section First_attempt.

      Lemma wf_LT : ∀ alpha: T1, nf alpha → Acc LT alpha.
    End First_attempt.

    Let Acc_strong (alpha:T1) :=
      ∀ n beta,
        nf (cons alpha n beta) → Acc LT (cons alpha n beta).

    Remark acc_impl {A} {R: A → A → Prop} (a b:A) :
      R a b → Acc R b → Acc R a.


    Lemma Acc_strong_stronger : ∀ alpha,
        nf alpha → Acc_strong alpha → Acc LT alpha.



    Lemma Acc_implies_Acc_strong : ∀ alpha,
        Acc LT alpha → Acc_strong alpha.

    Theorem nf_Acc (alpha : T1): nf alpha → Acc LT alpha.

  End well_foundedness_proof.
End Direct_proof.

Definition nf_Acc := Direct_proof.nf_Acc.

Corollary nf_Wf : well_founded_restriction _ nf lt.


Corollary T1_wf : well_founded LT.
Definition transfinite_recursor_lt :
  ∀ (P:T1 → Type),
    (∀ x:T1,
        (∀ y:T1, nf x → nf y → lt y x → P y) → P x) →
    ∀ alpha: T1, P alpha.


Definition transfinite_recursor := well_founded_induction_type T1_wf.

Check transfinite_recursor.


Import Direct_proof.

Ltac transfinite_induction_lt alpha :=
  pattern alpha; apply transfinite_recursor_lt.


Ltac transfinite_induction alpha :=
  pattern alpha; apply transfinite_recursor.

Lemma succ_nf : ∀ alpha : T1 , nf alpha → nf (succ alpha).

Lemma plus_zero alpha: zero + alpha = alpha.

Lemma plus_zero_r alpha: alpha + zero = alpha.


Lemma succ_is_plus_one (a : T1) : succ a = a + 1.

Lemma succ_of_plus_finite :
  ∀ a (H: nf a) (i:nat) , succ (a + i) = a + S i.

Lemma plus_cons_cons_rw1 :
  ∀ a n b a' n' b',
  lt a a' →
  cons a n b + cons a' n' b' = cons a' n' b'.

Lemma plus_cons_cons_rw2 :
  ∀ a n b n' b',
  nf (cons a n b) →
  nf (cons a n' b') →
  cons a n b + cons a n' b' = cons a (S (n + n')) b'.

Lemma plus_cons_cons_rw3 :
  ∀ a n b a' n' b',
  lt a' a →
  nf (cons a n b) →
  nf (cons a' n' b') →
  cons a n b + cons a' n' b'=
  cons a n (b + (cons a' n' b')).

Lemma ap_plus : ∀ a,
    ap a →
    ∀ b c,
      nf b → nf c → lt b a → lt c a → lt (b + c) a.

Lemma ap_plusR :
  ∀ c,
  nf c →
  c ≠ zero →
  (∀ a b, nf a → nf b → lt a c →lt b c → lt (a + b) c) →
  ap c.

Lemma plus_nf0 :
  ∀ a, nf a →
  ∀ b c,
    lt b (phi0 a) →
    lt c (phi0 a) →
    nf b → nf c →
    nf (b + c).


Lemma plus_nf:
  ∀ a, nf a → ∀ b, nf b → nf (a + b).

Lemma omega_term_plus_rw:
  ∀ a n b,
    nf (cons a n b) →
    omega_term a n + b = cons a n b.


Lemma plus_is_zero alpha beta :
  nf alpha → nf beta →
  alpha + beta = zero → alpha = zero ∧ beta = zero.

Lemma T1add_not_monotonous_l :
  ∃ a b c : T1, a t1< b ∧ a + c = b + c.

Lemma T1mul_not_monotonous :
  ∃ a b c : T1, c ≠ zero ∧ a t1< b ∧ a × c = b × c.

Lemma succ_strict_mono :
  ∀ a b,
    lt a b → nf a → nf b →
    lt (succ a) (succ b).

Lemma succ_strict_mono_LT :
  ∀ alpha beta,
  alpha t1< beta → succ alpha t1< succ beta.

Lemma succ_mono :
  ∀ a b,
  nf a → nf b →
  leq lt a b → leq lt (succ a) (succ b).

Lemma lt_succ_le_R :
  ∀ a, nf a → ∀ b, nf b →
  leq lt (succ a) b → lt a b .

Lemma le_lt_LT alpha beta :
  nf alpha → nf beta → leq lt alpha beta → leq LT alpha beta.

Lemma LT_succ_LE_R :
  ∀ alpha beta,
    nf alpha →
    succ alpha t1≤ beta → alpha t1< beta.

Lemma lt_succ_le_2 :
  ∀ a,
  nf a → ∀ b, nf b →
  lt a (succ b) → leq lt a b.