# Library ssete9

Require Import ssreflect ssrfun ssrbool eqtype ssrnat.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

# prelude

Useful lemmas missing in ssreflect

Lemma if_simpl (p: bool): (if p then true else false) = p.
Proof. by case: p. Qed.

Lemma ltn_simpl1 n n': ((n' + n).+1 < n) = false.

Lemma eqn_simpl1 n n': ((n' + n).+1 == n) = false.

Lemma ltn_simpl2 n n' n'':
(n * n' + n + n' < n * n'' + n + n'') = (n' < n'').

Lemma eqn_simpl2 n n' n'':
(n * n' + n + n' == n * n'' + n + n'') = (n' == n'').

Lemma ltn_add_le m1 m2 n1 n2: m1 < n1 -> m2 <= n2 -> m1 + m2 < n1 + n2.
Proof. by move => pa pb; move: (leq_add pa pb); rewrite addSn. Qed.

Lemma ltn_add_el m1 m2 n1 n2: m1 <= n1 -> m2 < n2 -> m1 + m2 < n1 + n2.
Proof. by move => pa pb; move: (leq_add pa pb); rewrite addnS. Qed.

Lemma ltn_add_ll m1 m2 n1 n2: m1 < n1 -> m2 < n2 -> m1 + m2 < n1 + n2.
Proof. by move => pa pb; exact: (ltn_add_el (ltnW pa) pb). Qed.

The ssreflect comparison on nat is WF

Lemma lt_wf: well_founded (fun (a b:nat) => a < b).
Proof.
move => n; split;elim: n; first by move => y ; rewrite ltn0.
move => n H y; rewrite ltnS leq_eqVlt; case /orP; first by move => /eqP ->.
by apply: H.
Defined.

## Example 1

An example of function defined by transfinite induction using Fix
Module Wf_ex.

Definition f_spec f n :=
if n is m.+2 then (f (f m.+1).+1 ).+1 else 0.

Lemma f_spec_simp f n: (forall n, f n = f_spec f n) -> f n = n.-1.
Proof.
move => H; case: n; first by rewrite H.
elim; first by rewrite H.
by move => n Hr; rewrite H /f_spec Hr Hr /=.
Qed.

Lemma f0 n p: p <= n -> p.+2 <= n.+2.
Proof. by rewrite ltnS ltnS. Qed.

Definition f1 :
forall x, (forall z, z < x -> {y:nat |y <= z.-1}) ->
{y:nat | y <= x.-1}.
Proof.
case; [by exists 0 | case; first by exists 0 ].
move => n Hr.
move: (Hr _ (ltnSn n.+1)) => [y1 h1].
move: (Hr _ (f0 h1)) => [y2 h2].
exists y2.+1; apply: (leq_trans h2 h1).
Defined.

Definition f2 := Fix lt_wf _ f1.
Definition f (x:nat): nat := sval (f2 x).

Lemma f_eqn x: f2 x = f1 (fun y _ => f2 y).
Proof.
move: x; apply: (Fix_eq lt_wf).
case => //; case => //n p p' Hp.
rewrite /f1 Hp; case: (p' n.+1 (ltnSn n.+1)) => y Hy /=.
by rewrite Hp.
Qed.

Lemma f_correct n: f n = f_spec f n.
Proof.
case: n => //; case => // n.
rewrite /f_spec /f f_eqn /f1.
by case: (f2 n.+1) => y1 H1; case: (f2 y1.+1) => y2 H2.
Qed.

End Wf_ex.

## Example 2

Second example, f(n) = 1 + \sum(i < n) f(i)

Require Import fintype bigop.
Module Wfsum.

Definition psum (f: nat -> nat) n := \sum_(i< n) (f i).
Definition f_spec f:= forall n, f n = (psum f n).+1.

Lemma f_spec_simp f n: f_spec f -> f n = 2 ^ n.
Proof.
move => fs.
elim: n; first by rewrite fs /f_spec /psum big_ord0.
move => n Hrec.
by rewrite -/(psum f n) - fs Hrec addnn expnS mul2n.
Qed.

Lemma psum_exten n f g :
(forall k, k < n -> f k = g k) -> (psum f n).+1 = (psum g n).+1.
Proof.
move => h; rewrite /psum; congr S; apply: eq_big => // [] [i lin] _ /=.
by apply: h.
Qed.

Lemma lt_dec n m: {n <m} + {~~ (n < m) }.
Proof. by case: (n<m); [ left | right ]. Qed.

Definition extension (n : nat) (p : forall k : nat, k < n -> nat) k :=
match lt_dec k n with
| left x => p k x
| _ => 0 end.

Definition f1 (n : nat) (h : forall z : nat, z < n -> nat) :=
(psum (extension h) n).+1.

Definition f2 := Fix lt_wf _ f1.

Lemma f_eqn x: f2 x = f1 (n:=x) (fun y _ => f2 y).
Proof.
move: x; apply: (Fix_eq lt_wf) => n A B Hp; apply: psum_exten.
move => k _; rewrite /extension;case: (lt_dec k n) => // a; apply: Hp.
Qed.

Definition f (x:nat): nat := f2 x.

Lemma f_correct: f_spec f.
Proof.
move => n; rewrite /f f_eqn /f1; apply: psum_exten => k kn.
by rewrite /extension; case: (lt_dec k n) => //; rewrite kn.
Qed.

End Wfsum.

## Example 3

We consider here only even numbers, show that comparison is WF, define a function by transfinite induction and show it is correct.

Module Wf_ex3.

Definition lte n m := [&& ~~ odd n, ~~ odd m & n < m].

Lemma lte_wf: well_founded lte.
Proof.
suff: forall n, Acc lte n /\ Acc lte n.+1.
by move => h n; move: (h n) => [].
elim.
by split; split => y; rewrite /lte /= ? ltn0 andbF.
move => n [sa sb]; split; first by exact.
split => y; rewrite /lte /=; move => /and3P[oy on].
rewrite ltnS leq_eqVlt; case /orP; first by move => /eqP ->.
rewrite ltnS leq_eqVlt; case /orP; first by move => /eqP ->.
by move => yn; case sa; apply; rewrite /lte /= oy yn (negbNE on).
Qed.

Definition f_spec f n :=
if n is m.+4 then (f (f (m.+2)).*2.+2 ).+1 else 0.

Lemma f_spec_simp f n: ~~ odd n -> (forall n, ~~odd n -> f n = f_spec f n)
-> f n = (n.-1)./2.
Proof.
move => on h1.
have h2: forall n, f (n.*2) = f_spec f (n.*2).
by move => h; apply: h1; rewrite odd_double.
move: (odd_double_half n); rewrite (negbTE on) add0n => <-.
set m := (n./2).
move: m; case; first by rewrite h2.
elim; first by rewrite h2 /=.
move => k hk.
rewrite h2 /f_spec doubleS doubleS - (doubleS k) hk.
by rewrite doubleS /= uphalf_double - (doubleS k) hk doubleS /= uphalf_double.
Qed.

Lemma f_spec_simp1 f n: (forall n, ~~odd n -> f n = f_spec f n)
-> f (n.*2.+2) = n.
Proof. by move => h; rewrite f_spec_simp //= ?uphalf_double // odd_double. Qed.

Lemma f_spec_simp2 f n: (forall n, f n = f_spec f n) -> f(n.*2.+3) = n.
Proof.
move => h.
have hh: forall n, f (n.*2.+2) = n.
move => m; apply: f_spec_simp1 => k _; apply: h.
by elim: n; [ by rewrite h | move => n Hr; rewrite h /= Hr hh].
Qed.

Lemma f0a y n: odd n = false -> odd n.+2 \/ y <= (n.+2)./2.-1 ->
y <= n./2 /\ lte (y.*2).+2 n.+4.
Proof.
rewrite /lte /=; move =>h; rewrite h /= odd_double; case => // eq.
split => //=.
move: eq. rewrite - ltnS - ltn_double ltnS ltnS.
rewrite - {2} (odd_double_half n) h add0n //.
Qed.

Lemma f0b a b: odd a.*2.+2 \/ b <= (a.*2.+2)./2.-1 -> b <= a.
Proof. by rewrite /= odd_double doubleK; case. Qed.

Lemma f0c n: odd n = false -> lte n.+2 n.+4.
Proof. by move => h; rewrite /lte ltnS ltnS ltnS leqnSn /= h. Qed.

Lemma odd_dec n : {odd n} + {odd n = false}.
Proof. by case h: (odd n); [ left | right ]. Qed.

Definition f1 :
forall x, (forall z, lte z x -> {y:nat | odd z \/ y <= (z./2).-1}) ->
{y:nat | odd x \/ y <= (x./2).-1}.
Proof.
case; first by exists 0; right.
case; first by exists 0; left.
case; first by exists 0; right.
case; first by exists 0; left.
move => n Hr.
case (odd_dec n) => on; first by exists 0; left; rewrite /= on.
move: (Hr _ (f0c on)) => [y1 h1].
move: (f0a on h1) => [sa sb].
move: (Hr _ sb) => [y2 h2].
exists y2.+1; right; apply: (leq_trans (f0b h2) sa).
Defined.

Definition f2 := Fix lte_wf _ f1.
Definition f (x:nat): nat := sval (f2 x).

Lemma f_eqn x: f2 x = f1 (fun y _ => f2 y).
Proof.
move: x; apply: (Fix_eq lte_wf).
case => //; case => //; case => //; case => //.
move => n p p' Hp; rewrite /f1; case: (odd_dec n) => // on.
rewrite Hp; case: (p' n.+2 (f0c on)) => y Hy /=.
by case: (f0a on Hy) => a b; rewrite Hp.
Qed.

Lemma f_correct n: ~~odd n -> f n = f_spec f n.
Proof.
case: n;first by rewrite /f /= f_eqn.
case => //; case; first by rewrite /f /= f_eqn.
case => // n; rewrite /f_spec /f f_eqn /f1 /=.
case: (odd_dec n) => a b.
by move: (negbNE (negbNE b)); move /negP; case.
by case:(f2 n.+2) => x p /=;case: (f0a a p) => y q; case:(f2 x.*2.+2).
Qed.

End Wf_ex3.

## More on accessiblity

We show that there is no striclty decreasing function with domain nat
Section Sequences.

Variable A : Set.
Variable R : A -> A -> Prop.

Lemma acc_rec a b: R a b -> Acc R b -> Acc R a.
Proof. by move => rab arb;move: a rab; case: arb. Qed.

Hypothesis W : well_founded R.

Theorem not_decreasing :
~ (exists f : nat -> A, (forall i:nat, R (f i.+1) (f i))).
Proof.
case => f dec.
pose p a := Acc R a -> ~ exists i, a = f i.
have H: forall a, p a.
move => a; apply: (well_founded_ind W p) => x Hx ax [i egi].
move: (dec i); rewrite - egi => H1; move: (Hx _ H1 (acc_rec H1 ax)).
by case; exists (i.+1).
move: (H _ (W (f 0))); case; by exists 0.
Qed.

End Sequences.

We show here an induction principle; we could use it for ordinals in NF form.

Section restricted_recursion.

Variables (A:Type)(P:A->Prop)(R:A->A->Prop).

Definition restrict a b := [/\ P a, R a b & P b].

Definition well_founded_P := forall a, P a -> Acc restrict a.

Lemma P_well_founded_induction_type :
well_founded_P ->
forall Q : A -> Type,
(forall x : A, P x -> (forall y : A,P y-> R y x -> Q y) -> Q x) ->
forall a : A, P a -> Q a.
Proof.
move => W Q Ha a.
have wfr: well_founded restrict by move => b; split => y [ra _ _]; apply: W.
apply: (well_founded_induction_type wfr (fun x => P x -> Q x)).
by move => x Hb px; apply: Ha => // y py ry; apply: Hb.
Qed.

End restricted_recursion.

Module CantorOrdinal.

# The type T1

This type represents all ordinals less that ε 0 , via the Cantor Normal Form. More exactly cons a n b represents ω A * (n.+1) + B if a represents A and b represents B.

Inductive T1 : Set :=
zero : T1
| cons : T1 -> nat -> T1 -> T1.

## Equality

we define a boolean equality, the use the mechanism of canonical structures provided by ssreflect

Fixpoint T1eq x y {struct x} :=
match x, y with
| zero, zero => true
| cons a n b, cons a' n' b' => [&& T1eq a a', n== n' & T1eq b b' ]
| _, _ => false
end.

Lemma T1eqP : Equality.axiom T1eq.
Proof.
move=> n m; apply: (iffP idP) => [|<-].
elim: n m; first by case => [ // | a n b //].
move => a H1 n b H2 [] // a' n' b' /= /andP [/H1 -> /andP []].
by move => /eqP -> /H2 ->.
by elim: n => // t ct n a caa /=;rewrite ct caa eqxx.
Qed.

Canonical T1_eqMixin := EqMixin T1eqP.
Canonical T1_eqType := Eval hnf in EqType T1 T1_eqMixin.

Implicit Arguments T1eqP [x y].
Prenex Implicits T1eqP.

Lemma T1eqE a n b a' n' b':
(cons a n b == cons a' n' b') = [&& a == a', n== n' & b == b' ].
Proof. by []. Qed.

Delimit Scope cantor_scope with ca.
Open Scope cantor_scope.

Some definitions
• φ0(x) is cons x 0 zero , it represents ω x
• one is φ0(0)
• omega is φ0(1)
• bad is an example of an ordinal not in normal form
• fun n := \F n is the canonical injection of nat into T1
• the log of cons a n b is a
• an ordinal is AP if it is in the image of φ0.

Definition phi0 a := cons a 0 zero.
Definition one := cons zero 0 zero.
Definition T1omega := phi0 (phi0 zero).
Definition T1bad := cons zero 0 T1omega.
Definition T1nat (n:nat) : T1 :=
if n is p.+1 then cons zero p zero else zero.
Definition T1log a := if a is cons a _ _ then a else zero.
Definition T1ap x := if x is cons a n b then ((n==0) && (b==zero)) else false.

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

Lemma T1F_inj: injective T1nat.
Proof.
case; first by case => //; discriminate.
move => n; case; [discriminate | by move => m; case => ->].
Qed.

Lemma T1phi0_zero : phi0 zero = \F 1. Proof. by []. Qed.
Lemma T1phi0_zero' : phi0 zero = one. Proof. by []. Qed.
Lemma T1log_phi0 x : T1log (phi0 x) = x. Proof. by []. Qed.
Lemma T1ap_phi0 x: T1ap (phi0 x). Proof. by []. Qed.

## Order on T1

We give here a recursion definition of comparison. Essentially, φ0(x) is strictly increasing,

Fixpoint T1lt x y {struct x} :=
if x is cons a n b then
if y is cons a' n' b' then
if a < a' then true
else if a == a' then
if (n < n')%N then true
else if (n == n') then b < b' else false
else false
else false
else if y is cons a' n' b' then true else false
where "x < y" := (T1lt x y) : cantor_scope.

Definition T1le (x y :T1) := (x == y) || (x < y).
Notation "x <= y" := (T1le x y) : cantor_scope.
Notation "x >= y" := (y <= x) (only parsing) : cantor_scope.
Notation "x > y" := (y < x) (only parsing) : cantor_scope.

Lemma T1lenn x: x <= x.
Proof. by rewrite /T1le eqxx. Qed.

Hint Resolve T1lenn.

Lemma T1ltnn x: (x < x) = false.
Proof. by elim:x => //= a -> n b ->; rewrite ltnn ! if_same. Qed.

Lemma T1lt_ne a b : a < b -> (a == b) = false.
Proof. by case h: (a== b) => //; rewrite (eqP h) T1ltnn. Qed.

Lemma T1lt_ne' a b : a < b -> (b == a) = false.
Proof. rewrite eq_sym; apply /T1lt_ne. Qed.

Lemma T1ltW a b : (a < b) -> (a <= b).
Proof. by rewrite /T1le => ->; rewrite orbT. Qed.

Lemma T1le_eqVlt a b : (a <= b) = (a == b) || (a < b).
Proof. by []. Qed.

Lemma T1lt_neAle a b : (a < b) = (a != b) && (a <= b).
Proof.
by rewrite T1le_eqVlt; case h: (a < b);[ rewrite (T1lt_ne h) | case(a==b) ].
Qed.

Lemma T1ltn0 x: (x < zero) = false. Proof. by case: x. Qed.
Lemma T1le0n x: zero <= x. Proof. by case: x. Qed.
Lemma T1len0 x: (x <= zero) = (x == zero). Proof. by case: x. Qed.
Lemma T1lt0n x: (zero < x) = (x != zero). Proof. by case: x. Qed.

Lemma T1ge1 x: (one <= x) = (x != zero).
Proof. by case: x => // [] // [] // [] // []. Qed.

Lemma T1lt1 x: (x < one) = (x==zero).
Proof. by case: x => // [] // [] // [] // []. Qed.

Lemma T1nat_inc n p : (n < p)%N = (\F n < \F p).
Proof.
case: p => //; first by rewrite T1ltn0 ltn0.
by case: n => // n p //=; rewrite ltnS if_same if_simpl.
Qed.

This is an alternative version of less-or-equal

Lemma T1le_consE a n b a' n' b':
(cons a n b <= cons a' n' b') =
if a < a' then true
else if a == a' then
if (n < n')%N then true
else if (n == n') then b <= b' else false
else false.
Proof.
rewrite /T1le T1eqE /=.
case pa: (a<a');first by rewrite orbT.
case pb: (a==a') => //; case pc: (n<n')%N;first by rewrite orbT.
by case pd: (n==n').
Qed.

We have exactly one of: a is less than, greater than, or equal to b

Lemma T1lt_trichotomy a b: [|| (a< b), (a==b) | (b < a)].
Proof.
elim: a b; first by case; [rewrite eqxx // | move => a n b].
move => a Ha n b Hb [] // a' n' b' /=.
case /or3P: (Ha a'); [by move => -> | | by move => ->; rewrite !orbT ].
move => h; rewrite h (eqP h) T1ltnn eqxx.
case : (ltngtP n n'); [done | by rewrite !orbT | move => -> ].
by rewrite T1eqE !eqxx /= Hb.
Qed.

Lemma T1lt_anti b a: a < b -> (b < a) = false.
Proof.
elim: a b; first by move => b; rewrite T1ltn0.
move => a Ha n b Hb [] // a' n' b' /=.
case pa: (a < a').
rewrite (Ha _ pa); case aa: (a' == a) => // _.
by move: pa; rewrite (eqP aa) T1ltnn.
case aa: (a== a') => //.
rewrite (eqP aa) eqxx T1ltnn; rewrite (eq_sym n'); case: (ltngtP n n') => //.
by move => _; apply:Hb.
Qed.

Lemma T1leNgt a b: (a <= b) = ~~ (b < a).
Proof.
case /or3P: (T1lt_trichotomy a b).
- by move => h; rewrite (T1lt_anti h) (T1ltW h).
- by move /eqP ->; rewrite T1ltnn T1lenn.
- by move => h; rewrite h /T1le (T1lt_anti h) (T1lt_ne' h).
Qed.

Lemma T1ltNge a b: (a < b) = ~~ (b <= a).
Proof. by rewrite T1leNgt negbK. Qed.

Lemma T1eq_le m n : (m == n) = ((m <= n) && (n <= m)).
Proof.
rewrite /T1le (eq_sym n m);case eqmn: (m == n) => //=.
by case lt1: (m < n) => //; rewrite (T1lt_anti lt1).
Qed.

Lemma T1le_total m n : (m <= n) || (n <= m).
Proof.
by rewrite /T1le;case /or3P: (T1lt_trichotomy m n) => -> //; rewrite !orbT.
Qed.

The next three definitions are similar to to those defined in ssrnat. we shall use T1ltgtP a lot.

CoInductive T1ltn_xor_geq m n : bool -> bool -> Set :=
| T1LtnNotGeq of m < n : T1ltn_xor_geq m n false true
| T1GeqNotLtn of n <= m : T1ltn_xor_geq m n true false.

CoInductive T1leq_xor_gtn m n : bool -> bool -> Set :=
| T1GeqNotGtn of m <= n : T1leq_xor_gtn m n true false
| T1GtnNotLeq of n < m : T1leq_xor_gtn m n false true.

CoInductive compare_T1 m n : bool -> bool -> bool -> Set :=
| CompareT1Lt of m < n : compare_T1 m n true false false
| CompareT1Gt of m > n : compare_T1 m n false true false
| CompareT1Eq of m = n : compare_T1 m n false false true.

Lemma T1leP x y : T1leq_xor_gtn x y (x <= y) (y < x).
Proof.
by rewrite T1ltNge; case le_xy: (x <= y); constructor;rewrite // T1ltNge le_xy.
Qed.

Lemma T1ltP m n : T1ltn_xor_geq m n (n <= m) (m < n).
Proof. by case T1leP; constructor. Qed.

Lemma T1ltgtP m n : compare_T1 m n (m < n) (n < m) (m == n).
Proof.
rewrite T1lt_neAle T1eq_le;case: T1ltP; first by constructor.
by rewrite T1le_eqVlt orbC; case: T1leP; constructor; first exact /eqP.
Qed.

We show here transitivity of comparison, using T1ltgtP .

Lemma T1lt_trans b a c: a < b -> b < c -> a < c.
Proof.
elim: c a b => [a [] // | a'' Ha n'' c'' Hc a [] ]; rewrite ? T1ltn0 //.
move => a' n' b'; case: a => // a n b /=.
case: (T1ltgtP a a') => h1 //.
case: (T1ltgtP a' a'') => h2 //; first by rewrite (Ha _ _ h1 h2).
by rewrite - h2 h1.
rewrite h1; case: (T1ltgtP a' a'') => // _; case: (ltngtP n n')%N => // h2.
case: (ltngtP n' n'') => h3 //; first by rewrite (ltn_trans h2 h3).
by rewrite - h3 h2.
by rewrite h2; case: (ltngtP n' n'') => h3 //; apply: Hc.
Qed.

Lemma T1lt_le_trans b a c: a < b -> b <= c -> a < c.
Proof.
by move => lab; case /orP;[ move /eqP => <- | apply:T1lt_trans].
Qed.

Lemma T1le_lt_trans b a c: a <= b -> b < c -> a < c.
Proof. by case /orP;[ move /eqP => <- |apply:T1lt_trans]. Qed.

Lemma T1le_trans b a c: a <= b -> b <= c -> a <= c.
Proof.
case /orP; first by move /eqP => ->.
by move => l1 l2; rewrite /T1le (T1lt_le_trans l1 l2) orbT.
Qed.

The following lemma implies x < ω x, so all ordinals are less than ε 0

Lemma head_lt_cons a n b: a < cons a n b.
Proof. by elim : a n b => // a Ha n b _ n' b' /=; rewrite (Ha n b). Qed.

Lemma T1lt_cons_le a n b a' n' b': (cons a n b < cons a' n' b') -> (a <= a').
Proof. by rewrite /T1le /=; case (T1ltgtP a a'). Qed.

Lemma T1le_cons_le a n b a' n' b': (cons a n b <= cons a' n' b') -> (a <= a').
Proof.
case /orP; [ by case /eqP => -> | apply:T1lt_cons_le ].
Qed.

Lemma phi0_lt a b: (phi0 a < phi0 b) = (a < b).
Proof. by rewrite /phi0 /= if_same if_simpl. Qed.

Lemma phi0_le a b: (phi0 a <= phi0 b) = (a <= b).
Proof. by rewrite /T1le phi0_lt /phi0 T1eqE eqxx andbT. Qed.

Lemma phi0_lt1 a n b a': (cons a n b < phi0 a') = (a < a').
Proof. by rewrite /phi0/= T1ltn0 !if_same if_simpl. Qed.

## Normal form

There exists a strictly infinite decreasing sequence of ordinals, so the order is not well founded

Theorem lt_not_wf : ~ (well_founded T1lt).
Proof.
set f := (fix f i := if i is n.+1 then cons zero 0 (f n) else T1omega).
by case/not_decreasing; exists f; elim.
Qed.

We say that cons a n b is NF if )b <φ0(a). If b is cons a' n' b', this says that b is less than b'. If a is zero, this says that b=0.

Fixpoint T1nf x :=
if x is cons a _ b then [&& T1nf a, T1nf b & b < phi0 a ]
else true.

Lemma T1nf_cons0 a n: T1nf a -> T1nf (cons a n zero).
Proof. by rewrite /= andbT. Qed.

Lemma T1nf_cons_cons a n a' n' b' : T1nf (cons a n (cons a' n' b')) -> a' < a.
Proof. by rewrite /= T1ltn0 !if_same if_simpl => /and3P [_ _]. Qed.

Lemma T1nf_consa a n b: T1nf (cons a n b) -> T1nf a.
Proof. by move /and3P => []. Qed.

Lemma T1nf_consb a n b: T1nf (cons a n b) -> T1nf b.
Proof. by move /and3P => []. Qed.

Lemma T1nf_finite1 n b: T1nf (cons zero n b) = (b == zero).
Proof. by case: b => // a n' b /=; rewrite !T1ltn0 !if_same andbF. Qed.

Lemma T1nf_finite n b: T1nf (cons zero n b) -> (b = zero).
Proof. by rewrite T1nf_finite1 => /eqP. Qed.

Lemma T1nfCE: ~~(T1nf T1bad). Proof. by []. Qed.

We show here that the restriction of T1lt to NF ordinals is well-founded, then prove two induction principles. Note that nf_Wf' says every NF x is accessible by the relation: u<v, u and v NF. If x is not NF it is trivially accessible. The proof is a bit tricky

Lemma nf_Wf : well_founded (restrict T1nf T1lt).
Proof.
have az: Acc (restrict T1nf T1lt) zero by split => y [_]; rewrite T1ltn0.
elim;[ exact az | move => a Ha n b _].
elim:{a} Ha n b => a Ha Hb n b.
case nx: (T1nf (cons a n b)); last by split => y [_ _]; rewrite nx.
move/and3P: (nx);rewrite -/T1nf; move => [na nb lba].
have aca: Acc (restrict T1nf T1lt) a by split.
have Hc: forall b, Acc (restrict T1nf T1lt) b ->
T1nf (cons a 0 b)-> Acc (restrict T1nf T1lt) (cons a 0 b).
move => c; elim => {c} c qa qb qc; split; case; first by move => _; apply: az.
move => a'' n'' b'' [] sa /= ua /and3P [_ nc _];move/and3P:(sa) => [ra rb _].
move: ua;case: (T1ltgtP a'' a) => ua ub.
- by apply: Hb.
- by case ub.
- by move: ub sa; case ee:(n''==0); [rewrite ua (eqP ee) => ub; apply: qb | ].
have Hd: forall b, T1nf b -> b < phi0 a -> Acc (restrict T1nf T1lt) b.
case; [by move => _ _ ; apply: az | move => a' n' b' nx'].
rewrite phi0_lt1 => aa'.
by apply: Hb; rewrite /restrict (T1nf_consa nx') na aa'.
elim: n b {nb lba} (Hd _ nb lba) nx => [ // | n He b]; elim.
move => c _ qb np; split; case; first by move => _; apply: az.
move => a'' n'' b'' [sa /= sb _];move /and3P: (sa) => [ra rb rc].
move: sb; case: (T1ltgtP a'' a) => sc sb; [ by apply: Hb | by case sb |].
move: sb; case: (ltngtP n'' n.+1); [rewrite ltnS leq_eqVlt | done | move ->].
rewrite sc in rc; move => sb _; move: sa; case /orP: sb.
move => /eqP ->; rewrite sc; apply: (He b'' (Hd _ rb rc)).
move => qd qe.
have nc0: T1nf (cons a n zero) by rewrite /= andbT.
apply: (acc_rec (And3 qe _ nc0) (He _ az nc0)).
by rewrite /= qd sc eqxx T1ltnn.
move => sb; move/and3P: np => [pa pb pc].
rewrite sc;apply: (qb _ (And3 rb sb pb)); rewrite -sc //.
Qed.

Lemma nf_Wf' : well_founded_P T1nf T1lt.
Proof. move => x /= nx; apply: nf_Wf. Qed.

Lemma T1transfinite_induction P:
(forall x, T1nf x -> (forall y, T1nf y -> y < x -> P y) -> P x) ->
forall a, T1nf a -> P a.
Proof.
move => H; exact: (P_well_founded_induction_type nf_Wf' H).
Qed.

Lemma T1transfinite_induction_Q (P: T1 -> Type) (Q: T1 -> Prop):
(forall x:T1, Q x -> T1nf x ->
(forall y:T1, Q y -> T1nf y -> y < x -> P y) -> P x) ->
forall a, T1nf a -> Q a -> P a.
Proof.
pose q a:= T1nf a /\ Q a; pose lt x y := x < y.
move => H a pa pb; move: {pa pb} a (conj pa pb).
have wf1: well_founded_P q lt.
move => a qa; elim: (nf_Wf' (proj1 qa)).
by move => b _ h2; split => c [ [na _] la [nb _]]; apply: h2.
have H': forall x, q x -> (forall y, q y -> lt y x -> P y) -> P x.
by move => x [pa pb] ha; apply: H => // y ya yb; apply: ha.
exact: (P_well_founded_induction_type wf1 H').
Qed.

Lemma T1nf_rect (P : T1 -> Type):
P zero ->
(forall n: nat, P (cons zero n zero)) ->
(forall a n b n' b', T1nf (cons a n b) ->
P (cons a n b) ->
b' < phi0 (cons a n b) ->
T1nf b' ->
P b' ->
P (cons (cons a n b) n' b')) ->
forall a, T1nf a -> P a.
Proof.
move =>H0 Hfinite Hcons; elim => // a IH1 n t IH2;case: a IH1.
by rewrite T1nf_finite1; move => _ /eqP ->.
move => a' n' c pa =>/and3P [pc pd pe]; auto.
Qed.

## Successor

We say that cons a n b is
• limit if a is non-zero, b is limit or zero
• finite if a is zero
• a successor if a is zero or b is a successor
and define its
• successor as \F (n+2) or cons a n (succ b)
• predecessor as \F n or cons a n (pred b)
• split u,v as cons a n x, y if b split as x,y and a is non-zero; and as 0,n+1 if a is zero
Note that if a=0, the quantity b is ignored; but when x is NF, then b is zero.

Fixpoint T1limit x :=
if x is cons a n b then
if a==zero then false else (b== zero) || T1limit b
else false.

Definition T1finite x := if x is cons a n b then a == zero else true.

Fixpoint T1is_succ x :=
if x is cons a n b then (a==zero) || T1is_succ b else false.

Fixpoint T1succ (c:T1) : T1 :=
if c is cons a n b
then if a == zero then cons zero n.+1 zero else cons a n (T1succ b)
else one.

Fixpoint T1pred (c:T1) : T1 :=
if c is cons a n b then
if (a==zero) then \F n else (cons a n (T1pred b))
else zero.

Fixpoint T1split x:=
if x is cons a n b then
if a==zero then (zero, n.+1) else
let: (x, y) := T1split b in (cons a n x,y)
else (zero,0).

Lemma split_limit x: ((T1split x).2 == 0) = ((x==zero) || T1limit x).
Proof.
elim: x => // a _ n b Hb /=.
case pa: (a==zero) => //; rewrite - Hb; by case: (T1split b).
Qed.

Lemma split_is_succ x: ((T1split x).2 != 0) = (T1is_succ x).
Proof.
elim: x => // a _ n b Hb /=.
case pa: (a==zero) => //; rewrite - Hb; by case: (T1split b).
Qed.

Lemma split_finite x: ((T1split x).1 == zero) = T1finite x.
Proof.
by case: x => // a n b /=; case pa: (a==zero) => //; case: (T1split b).
Qed.

Lemma split_succ x: let:(y,n):= T1split x in T1split (T1succ x) = (y,n.+1).
Proof.
elim: x => // a _ n b /=.
by case pa: (a==zero) => //=; rewrite pa /=; case: (T1split b) => u v ->.
Qed.

Lemma split_pred x: let:(y,n):= T1split x in T1split (T1pred x) = (y,n.-1).
Proof.
elim: x => // a _ n b /=.
case pa: (a==zero) => //=; first by case: n.
by rewrite pa /=; case:(T1split b) => // u v ->.
Qed.

Lemma split_le x : (T1split x).1 <= x.
Proof.
elim: x => // a _ n b Hb /=.
case pa: (a==zero) => //; move: Hb; case: (T1split b) => y m /=.
by rewrite T1le_consE !eqxx /= => ->; rewrite !if_same.
Qed.

Lemma nf_split x : T1nf x -> T1nf (T1split x).1.
Proof.
elim: x => // a _ n b Hb /=.
case pa: (a==zero) => // /and3P [sa /Hb sb sc] /=.
move: (T1le_lt_trans (split_le b) sc).
by move: sb; case (T1split b) => y m /= -> ->; rewrite sa.
Qed.

Lemma T1finite1 n: T1finite (\F n).
Proof. by case:n. Qed.

Lemma T1finite2 x: T1finite x -> T1nf x -> x = \F ((T1split x).2).
Proof. by case: x => // a n b /eqP -> /T1nf_finite ->. Qed.

Proof. by split => //; case. Qed.

Lemma T1finite_succ x: T1finite x -> T1finite (T1succ x).
Proof. elim: x => // a Ha n b Hb; move /eqP => -> //. Qed.

Lemma T1succ_nat n: T1succ (\F n) = \F (n.+1).
Proof. by case: n. Qed.

Lemma nf_omega : T1nf T1omega. Proof. by []. Qed.
Lemma nf_finite n: T1nf (\F n). Proof. by case: n. Qed.
Lemma nf_phi0 a: T1nf (phi0 a) = T1nf a. Proof. by rewrite /= andbT. Qed.
Lemma nf_log a: T1nf a -> T1nf (T1log a).
Proof. by case: a => // a n b /T1nf_consa. Qed.

An ordinal is zero, limit or a successor, exclusively. When we split x the first component is zero or limit, the second is a natural number

Lemma limit_pr1 x: (x == zero) (+) (T1limit x (+) T1is_succ x).
Proof.
elim: x => //a _ n b Hb /=; case az: (a== zero) => //.
by case bz: (b == zero); [ rewrite (eqP bz) | move: Hb; rewrite bz].
Qed.

Lemma split_limit1 x (y:= (T1split x).1): (y == zero) || (T1limit y).
Proof.
rewrite /y;elim x => // a _ n b Hb /=.
by case pa: (a==zero) => //; move: Hb; case (T1split b) => u v /=; rewrite pa.
Qed.

If x is limit, if y is less than x, so is the successor of y

Lemma limit_pr x y: T1limit x -> y < x -> T1succ y < x.
Proof.
elim: x y; [ by [] |move => a _ n b Hb y /= H1].
case: y; [ by move => _; move: H1; case: a |move => a' n' b' /=].
have aux: b' < b -> T1succ b' < b.
case: (a==zero) H1 => // /orP []; first by move => /eqP ->; rewrite T1ltn0.
by apply: Hb.
case a'; first by rewrite /T1succ; move => _;move: H1; case: a.
move => a'' n'' b''; case: a H1; [ done | move => u v w _ ].
simpl; rewrite T1eqE;case: (a'' < u) => //; case: eqP => // _.
case:(n'' < v)%N => //; case e2: (n'' == v) => //; case: (b'' < w) => //.
by case: eqP => //= _; case: (n' <n)%N => //; case: eqP.
Qed.

Lemma pred_le a: T1pred a <= a.
Proof.
elim: a => // a _ n b Hb /=; case az: (a==zero).
by rewrite (eqP az); case: n => // m /=; rewrite T1le_consE /= ltnS leqnn.
by rewrite T1le_consE /= Hb !eqxx !if_same.
Qed.

Lemma pred_lt a: T1is_succ a -> T1pred a < a.
Proof.
elim: a => // a _ n b Hb /=; case az: (a==zero).
by rewrite (eqP az); case: n => // m /=; rewrite ltnS leqnn.
by move /Hb;rewrite /=T1ltnn ltnn !eqxx.
Qed.

Lemma succ_lt a: a < T1succ a.
Proof.
elim: a => // a asa n b bb;move: asa; case: a; first by rewrite /= ltnSn.
by move => u v w h /=; rewrite bb ! eqxx !ltnn if_same.
Qed.

Lemma nf_succ a: T1nf a -> T1nf (T1succ a).
Proof.
elim:a => // a _ n b Hb /and3P [pa /Hb pb pc] /=.
case az: (a== zero) => //; apply /and3P;split => //.
by apply:limit_pr => //=; rewrite az.
Qed.

Lemma nf_pred a: T1nf a -> T1nf (T1pred a).
Proof.
elim:a => // a _ n b Hb /and3P [pa /Hb pb pc] /=.
case az: (a== zero) => //; first by apply: nf_finite.
by rewrite /= (T1le_lt_trans (pred_le b) pc) pb !andbT.
Qed.

Lemma succ_pred x: T1nf x -> T1is_succ x -> x = T1succ (T1pred x).
Proof.
elim: x => // a _ n b Hb; case az: (a==zero).
by rewrite (eqP az) T1nf_finite1 => /eqP ->; case: n.
by move => /T1nf_consb /Hb h /=;rewrite /= az /= az => h'; rewrite - h.
Qed.

Proof. by split => //; case => //; case. Qed.

Lemma succ_p1 x: T1is_succ (T1succ x).
Proof.
by elim: x => // a _ n b Hb /=; case pa: (a==zero) => //=; rewrite pa.
Qed.

Lemma pred_succ x: T1nf x -> T1pred (T1succ x) = x.
Proof.
elim: x => // a _ n b Hb nx /=; case az: (a==zero).
by move: nx; rewrite (eqP az) T1nf_finite1 => /eqP ->.
by rewrite /= az (Hb (T1nf_consb nx)).
Qed.

Proof. discriminate. Qed.

Lemma succ_inj x y: T1nf x -> T1nf y -> (T1succ x == T1succ y) = (x==y).
Proof.
move => nx ny;case h: (T1succ x == T1succ y).
by rewrite - (pred_succ nx) (eqP h) (pred_succ ny) eqxx.
by case hh: (x==y) => //; rewrite -h (eqP hh) eqxx.
Qed.

Proof. done. Qed.

Lemma lt_succ_succ x y: T1succ x < T1succ y -> x < y.
Proof.
elim: x y; first by case; [ rewrite T1ltnn | move => a n b _ ].
move => a _ n b Hb; case; [ by case a | move => a' n' b'].
case a;case a' => //; first by rewrite /= ltnS if_same; case: (n < n')%N.
move => a'' n'' b'' a''' n''' b'''; rewrite /= T1eqE.
case (T1ltgtP a''' a'') => //;case (ltngtP n''' n'') => //.
case (T1ltgtP b''' b'') => //;case (ltngtP n n') => //= _ _ _ _; apply: Hb.
Qed.

Lemma le_succ_succ x y: x <= y -> T1succ x <= T1succ y.
Proof. rewrite !T1leNgt; apply: contra; exact:lt_succ_succ. Qed.

Proof. done. Qed.

Lemma lt_succ_succE x y:
T1nf x -> T1nf y -> (T1succ x < T1succ y) = (x < y).
Proof.
move => nx ny.
case (T1ltgtP (T1succ x) (T1succ y)).
+ by move/lt_succ_succ => ->.
+ by move /lt_succ_succ => /T1lt_anti.
+ by move /eqP; rewrite (succ_inj nx ny) => /eqP ->; rewrite T1ltnn.
Qed.

Some properties of comparison and successor

Lemma le_succ_succE x y:
T1nf x -> T1nf y -> (T1succ x <= T1succ y) = (x <= y).
Proof.
by move => na nb; rewrite /T1le (succ_inj na nb) (lt_succ_succE na nb).
Qed.

Lemma lt_succ_le_1 a b : T1succ a <= b -> a < b.
Proof. apply: T1lt_le_trans (succ_lt a). Qed.

Lemma lt_succ_le_2 a b: T1nf a -> a < T1succ b -> a <= b.
Proof.
elim: a b; first by move => b;rewrite T1le0n.
move => a' _ n' b' Hb; case; first by rewrite /= ! T1ltn0 ! if_same.
case.
case a' => // n b; move /T1nf_finite ->.
rewrite /= if_same if_simpl ltnS T1le_consE T1le0n T1ltnn eqxx leq_eqVlt.
case: (ltngtP n' n) => //.
move => a'' n'' b'' n b /T1nf_consb H; rewrite T1le_consE /=.
case: (T1ltgtP a' (cons a'' n'' b'')) => //.
by case: (ltngtP n' n) => //= _ _; apply: Hb.
Qed.

Lemma lt_succ_le_3 a b: T1nf a -> (a < T1succ b) = (a <= b).
Proof.
move => na; case h:(a < T1succ b).
by rewrite (lt_succ_le_2 na h).
rewrite - h; case: (T1ltP b a) => // ab; exact: (T1le_lt_trans ab (succ_lt b)).
Qed.

Lemma lt_succ_le_4 a b: T1nf b -> (a < b) = (T1succ a <= b).
Proof.
move => nb.
case: (T1ltP a b).
rewrite T1leNgt T1ltNge; case h: (b < T1succ a) => //.
by rewrite(lt_succ_le_2 nb h).
by move /le_succ_succ => /(T1lt_le_trans (succ_lt b)); rewrite T1leNgt => ->.
Qed.

Lemma phi0_log a: a < phi0 (T1succ (T1log a)).
Proof. by case: a => // a n b /=; rewrite succ_lt. Qed.

Lemma tail_lt_cons a n b: b < phi0 a -> b < cons a n b.
Proof.
case b => // a' n' b' /=.
by case: (T1ltgtP a' a) => //; rewrite T1ltn0 if_same.
Qed.

The definition of addition and subtraction given here are straightforward given our interpretation of cons

if x is cons a n b then
if y is cons a' n' b' then
if a < a' then cons a' n' b'
else if a' < a then (cons a n (b + (cons a' n' b')))
else (cons a (n+n').+1 b')
else x
else y
where "a + b" := (T1add a b) : cantor_scope.

Fixpoint T1sub x y :=
if x is cons a n b then
if y is cons a' n' b' then
if x < y then zero
else if a' < a then cons a n b
else if (n < n')%N then zero
else if (a==zero) then
if (n ==n') then zero else cons zero ((n-n').-1) zero
else if (n == n') then b - b' else cons a (n-n').-1 b
else x
else zero
where "x - y" := (T1sub x y):cantor_scope.

Easy properties

Lemma succ_is_add_one a: T1succ a = a + one.
Proof.
by elim:a => // a _ n b Hb /=; rewrite T1ltn0 addn0 Hb; case a.
Qed.

Lemma add1Nfin a: ~~ T1finite a -> one + a = a.
Proof. by case a => // u v w /=; case u. Qed.

Lemma sub1Nfin a: ~~ T1finite a -> a - one = a.
Proof. by case: a => // u v w /=; case:u. Qed.

Lemma sub1a x: x != zero -> T1nf x -> x = one + (x - one).
Proof.
move => na nb;case fb:(T1finite x).
move: na fb nb ; case: x => // a' n' b' /= _ /eqP ->.
by rewrite T1lt1 => /and3P [_ _ /eqP ->]; case: n'.
rewrite sub1Nfin ?fb // add1Nfin // fb //.
Qed.

Lemma sub1b x: T1nf x -> x = (one + x) - one.
Proof.
case:x => // a n b; case: a => //; rewrite T1nf_finite1 => /eqP -> //.
Qed.

Lemma sub_1aCE (a:= cons zero 0 T1bad) : one + (a - one) != a.
Proof. done. Qed.

Lemma sub_1bCE (a:= cons zero 0 T1bad) : (one + a - one) != a.
Proof. done. Qed.

Lemma T1subn0 x: x - zero = x.
Proof. by case: x. Qed.

Lemma T1subnn x: x - x = zero.
Proof.
by elim:x => // a _ n b Hb /=; rewrite !T1ltnn ltnn !eqxx Hb if_same.
Qed.

Lemma add_int n m : \F n + \F m = \F (n +m)%N.
Proof.
case: n m => // n; case; first by rewrite addn0 T1addn0.
by move => m /=; rewrite - addnS.
Qed.

Lemma sub_int n m : \F n - \F m = \F (n -m)%N.
Proof.
case: n m => // n [] // m /=.
rewrite subSS /T1nat; case (ltngtP n m) => pa.
- by rewrite (eqP (ltnW pa)).
- by rewrite -(subnSK pa).
- by rewrite pa subnn.
Qed.

Lemma add_fin_omega n: \F n + T1omega = T1omega.
Proof. by case: n. Qed.

~~T1limit x /\(forall u v, T1limit u -> x <> u + \F v.+1).
Proof. by split => // u v; case u => // a n b; case a. Qed.

Lemma split_add x: let: (y,n) :=T1split x in T1nf x ->
(x == y + \F n) && ((y==zero) || T1limit y ).
Proof.
elim: x => //a _ n b Hb /=.
case pa: (a==zero).
by rewrite (eqP pa) T1lt1 => /and3P [_ _ /eqP ->]; rewrite !eqxx.
move: Hb; case: (T1split b) => y s h /and3P [_ /h/andP [/eqP -> sb] _].
rewrite orFb /T1limit pa sb andbT; case: {h} s => //=; first by rewrite T1addn0.
by move => m; move: pa; case: a.
Qed.

b < phi0 a -> cons a n zero + b = cons a n b.
Proof.
by case: b => // u v w; rewrite phi0_lt1 /= => h; rewrite h (T1lt_anti h).
Qed.

Lemma addC_CE (a := one) (b := T1omega):
[/\ T1nf a, T1nf b & a + b <> b + a].
Proof. by split. Qed.

We say that x is AP is the sum of two ordinals less than x is less than x. This conditionq holds if x has the form )φ0(a); the converse is true when x is non-zero. We may also assume everything NF.

Lemma ap_pr0 a (x := phi0 a) b c:
b < x -> c < x -> b + c < x.
Proof.
case: b c; [by move => c |move => a1 n b].
case; [by move => H _ | move => a' n' c'].
by rewrite ! (fun_if (fun z => z < x)) !phi0_lt1 if_same; case: (a1 < a').
Qed.

Lemma ap_pr1 c:
(forall a b, a < c -> b < c -> a + b < c) ->
(c== zero) || T1ap c.
Proof.
case: c => // a n b.
case: n b => [b H | n b H]; last first.
have l2: (cons a n b) < (cons a n.+1 b) by rewrite /= eqxx ltnS leqnn if_same.
move: (H _ _ l2 l2); rewrite /= !T1ltnn /= !T1ltnn eqxx if_same.
case bz: (b == zero) => //.
have pa: cons a 0 zero < cons a 0 b by move: bz;rewrite /= !T1ltnn eqxx; case b.
by move: (H _ _ pa pa); rewrite /= T1ltnn /= T1ltnn if_same.
Qed.

Lemma ap_pr2 c:
T1nf c -> c <> zero ->
(forall a b, T1nf a -> T1nf b -> a < c -> b < c -> a + b < c) ->
T1ap c.
Proof.
case: c => // a n b nc _ Hr.
have {Hr} H: forall u, T1nf u -> u < cons a n b -> u + u < cons a n b.
by move => u ua ub; apply: Hr.
case: n b H nc => [b H /T1nf_consa na | n b H nc].
have nc: T1nf (cons a 0 zero) by rewrite /= andbT.
move: (H _ nc); rewrite /= T1ltnn eqxx /= if_same T1ltnn.
by case b => // u v w; apply.
have l2: (cons a n b) < (cons a n.+1 b) by rewrite /= T1ltnn eqxx ltnSn.
move: (H (cons a n b) nc l2).
by rewrite /= T1ltnn /= !T1ltnn /= eqxx if_same ltnS -{3}(add0n n) ltn_add2r.
Qed.

Lemma ap_pr2CE (c := cons T1bad 1 zero):
(forall a b, T1nf a -> T1nf b -> a < c -> b < c -> a + b < c).
Proof.
move => a b na nb; rewrite /c.
move: na nb;case: a; first by rewrite T1add0n.
move => a' n' b' HA; case: b; first by rewrite T1addn0.
move => a'' n'' b'' HB.
have pa: (a' == T1bad) = false.
by apply /negP => /eqP ba; move: HA; rewrite ba /=.
have pb: (a'' == T1bad) = false.
by apply /negP => /eqP ba; move: HB; rewrite ba /=.
rewrite /= !(fun_if (fun z => z < cons T1bad 1 zero)) /= pa pb => sa sb.
by case (T1ltgtP a' a'').
Qed.

Alternate definition of an AP: if a<x then a+x=x.

Lemma add_simpl1 a n b n' b': a != zero ->
cons a n b + cons zero n' b' = cons a n (b + cons zero n' b').
Proof. by case: a. Qed.

Lemma add_simpl2 n b a' n' b': a' != zero ->
cons zero n b + cons a' n' b' = cons a' n' b'.
Proof. by case: a'. Qed.

Lemma ap_pr3 a b (x := phi0 a): b < x -> b + x = x.
Proof.
by rewrite /x /phi0; case: b => // a' n' b'; rewrite phi0_lt1 /= => ->.
Qed.

Lemma ap_pr4 x: (forall b, b < x -> b + x = x) -> (x == zero) || T1ap x.
Proof.
case: x => // a; case; [ case => // a' n' b' H | move => n b H].
have: cons a 0 zero < cons a 0 (cons a' n' b') by rewrite /= T1ltnn eqxx.
move /H;rewrite /= T1ltnn; discriminate.
have: cons a n zero < cons a n.+1 b by rewrite /= T1ltnn eqxx ltnSn.
by move /H; rewrite /= T1ltnn - {3} (addn0 n); case => /eqP; rewrite eqn_add2l.
Qed.

It follows tthat the sum of two NF ordinals is NF

Lemma nf_add a b: T1nf a -> T1nf b -> T1nf (a + b).
Proof.
elim: a b => // a Ha n b Hb [] // a' n' b' ha hb /=.
case (T1ltgtP a a') => //;last by move => ->; move: hb.
rewrite -(phi0_lt1 _ n' b') => pb.
by move: ha => /= /and3P [-> sb sc]; rewrite (Hb _ sb hb) ap_pr0.
Qed.

Lemma T1add_eq0 m n: (m + n == zero) = (m == zero) && (n == zero).
Proof.
case: m; [by rewrite T1add0n | move => a' n' b'; rewrite andFb].
by case: n => // a n b /=; case (T1ltgtP a a').
Qed.

Lemma add_le1 a b: a <= a + b.
Proof.
elim:a b; first by rewrite /T1le /=; case;[ rewrite eqxx | ].
move => a' _ n' b' Hb [] // a n b /=.
case: (T1ltgtP a' a) => h;rewrite T1le_consE ?h // ? ltnn T1ltnn !eqxx //=.
Qed.

Lemma add_le2 a b: b <= a + b.
Proof.
case: a => // a' n' b'; case: b ; [done | move => a n b /=].
case: (T1ltgtP a' a) => // h;rewrite T1le_consE ?h // ltnS leq_addl /= eqxx.
by rewrite if_same.
Qed.

Lemma minus_lt a b: a < b -> a - b = zero.
Proof.
elim: a b => // a' _ n' b' Hb [] // a'' n'' b'' h.
by rewrite /T1sub h.
Qed.

Lemma minus_le a b: a <= b -> a - b = zero.
Proof.
rewrite T1le_eqVlt;case /orP; [move /eqP ->; apply: T1subnn| apply: minus_lt].
Qed.

Lemma T1sub0 a: a - zero = a.
Proof. by case: a => // a n b; case: a. Qed.

Lemma nf_sub a b: T1nf a -> T1nf b -> T1nf (a - b).
Proof.
elim: a b => // a' _ n' b' Hb []; [ by rewrite T1sub0 | move => a n b /= sa sb].
have sc: T1nf (b' - b).
by move/and3P: sa => [_ nb _]; move/and3P: sb => [_ nb' _]; apply: Hb.
by rewrite 11!fun_if /= sa sc !if_same.
Qed.

Lemma sub_le1 a b : T1nf a -> (a - b) <= a.
Proof.
elim: a b => [b // | a' _ n' b' Hb].
case; [by rewrite T1sub0 T1lenn | move => a n b /and3P [_ /Hb la lb] /=].
set u := if a' <a then _ else _; case: u => //.
case: (a < a') => //; case: (ltngtP n' n) => // nn.
have hh: ((n' - n).-1 < n')%N.
move: nn; by case: n' => // n' h; rewrite subSn // ltnS leq_subr.
rewrite (fun_if (fun z => (z <= _))) !T1le_consE T1ltnn hh eqxx (eq_sym _ a').
by case (T1ltgtP a' zero).
case :eqP => // _.
apply: (T1le_trans (la b));exact:(T1ltW (tail_lt_cons n' lb)).
Qed.

Lemma sub_pr a b: T1nf b -> (a + b) - a = b.
Proof.
elim: a b; first by move => b _; rewrite T1sub0.
move => a' _ n' b' Hb; case; first by rewrite T1addn0 T1subnn.
move => a n b nb /=.
case (T1ltgtP a' a) => pa.
by rewrite /= pa (T1lt_anti pa) (T1lt_ne' pa).
have hh: a' == zero = false by move: pa; case a' => //; rewrite T1ltn0.
by rewrite /= !T1ltnn ltnn !eqxx /= T1ltNge add_le1 hh /= Hb.
by move: nb; case: eqP => // -> nb; rewrite (T1nf_finite nb).
Qed.

Lemma add_inj a b c : T1nf b -> T1nf c -> a + b = a + c -> b = c.
Proof.
move => sb sc h.
by rewrite - (sub_pr a sb) - (sub_pr a sc) h.
Qed.

Lemma sub_pr1 a b: T1nf b -> a <= b -> b = a + (b - a).
Proof.
move => nb; rewrite /T1le.
case: (altP (a =P b)) => [-> | _ /=]; first by rewrite T1subnn T1addn0.
move: nb; elim: a b; first by move => b nb; rewrite T1sub0 //.
move => a' _ n' b' Hb; case; [by rewrite T1ltn0 | move => a n b].
case: a; [ move => hb hc | move => a'' n'' b''].
move: hb hc => /=;rewrite T1lt1 => /andP [_ /eqP ->].
case a'=> //; rewrite !T1ltn0 eqxx if_same if_simpl => le1.
by rewrite (ltnNge) (ltnW le1) (gtn_eqF le1) /= - addSn - subnS (subnKC le1).
move => /and3P [_ sb sc].
move: (Hb _ sb) (T1le_lt_trans (sub_le1 b' sb) sc) => ha hb /=.
case (T1ltgtP a' (cons a'' n'' b'')) => //.
case a' => // a3 n3 b3 /=; rewrite T1eqE (eq_sym a'' a3) (eq_sym n'' n3).
case (T1ltgtP a3 a'') => //= pa; first by rewrite pa.
case (ltngtP n3 n'') => //= pb; first by rewrite pa T1ltnn eqxx pb.
by move => h; rewrite (T1lt_anti h) (T1lt_ne' h) pa pb T1ltnn ltnn ! eqxx h.
move ->;rewrite !T1ltnn ltnn !eqxx (eq_sym n n');case (ltngtP n' n) => //.
by rewrite T1ltnn => le1; rewrite - addSn - subnS (subnKC le1).
move => -> hw; rewrite (T1lt_anti hw); move: (ha hw) hb; clear hw.
case (b - b'); first by rewrite T1addn0 => ->.
by move => u v w; rewrite phi0_lt1 => <- ua; rewrite ua (T1lt_anti ua).
Qed.

Proof. done. Qed.

Lemma sub_pr1r a b: T1nf a -> a - b = zero -> a <= b.
Proof.
move => nn h; case /orP: (T1le_total a b) => // h1.
by move: (sub_pr1 nn h1); rewrite h T1addn0 => ->.
Qed.

Lemma omega_minus_one : T1omega - one = T1omega.
Proof. by []. Qed.

Lemma sub_nz a b: T1nf b -> a < b -> (b - a) != zero.
Proof.
move => nb lab; apply/negP => h.
by move: (sub_pr1r nb (eqP h)); rewrite T1leNgt lab.
Qed.

Lemma sub_nzCE (a := one) (b := (cons zero 0 one)):
(a < b) && (b-a == zero).
Proof. done. Qed.

Lemma T1addA c1 c2 c3: c1 + (c2 + c3) = (c1 + c2) + c3.
Proof.
elim: c1 c2 c3 => // a1 _ n1 b1 H; case.
move => a2 n2 b2; case;[ by rewrite ! T1addn0 | move => a3 n3 b3 /=].
case (T1ltgtP a2 a3).
+ case (T1ltgtP a1 a2) => pa pb /=.
- by rewrite (T1lt_trans pa pb) /= pb.
- by case (T1ltgtP a1 a3) => //; rewrite - H /= pb.
- by rewrite pa pb.
+ case (T1ltgtP a1 a2) => pa pb /=; move: (T1lt_anti pb) => pc.
- by rewrite pb pc.
- by move:(T1lt_trans pb pa) => h; rewrite h (T1lt_anti h) - H /= pb pc.
- by rewrite pa pb pc.
+ move => <-; case (T1ltgtP a1 a2) => pb /=.
- by rewrite !T1ltnn.
- by rewrite pb (T1lt_anti pb) - H /= !T1ltnn.
Qed.

Lemma T1addS a b : (a + T1succ b) = T1succ (a+ b).

Lemma T1le_add2l p m n : (p + m <= p + n) = (m <= n).
Proof.
elim:p m n => // a Ha n b Hb.
move => a' n' b'; case.
rewrite T1addn0 /=; case (T1ltgtP a a').
move => h; rewrite T1le_consE (T1lt_ne' h) (T1lt_anti h) => //.
move: (Hb (cons a' n' b') zero).
by rewrite T1le_consE T1addn0 T1ltnn ltnn ! eqxx => ->.
by rewrite T1le_consE T1ltnn eqxx addnC ltn_simpl1 eqn_simpl1.
move => a'' n'' b'' /=.
case (T1ltgtP a a');case (T1ltgtP a a'') =>// pa pb;
rewrite ? pa -? pa !T1le_consE ? (T1lt_anti pb) ? eqxx ? T1ltnn.
- move: (T1lt_trans pa pb) => pc.
by rewrite (T1lt_ne' pb) (T1lt_ne' pc) (T1lt_anti pc).
- by rewrite (T1lt_ne' pb).
- by rewrite pa (T1lt_trans pb pa).
- by rewrite Hb ltnn T1le_consE.
- by rewrite pb ltnS leq_addr.
- by rewrite -pb pa.
- by rewrite -pb addnC ltn_simpl1 eqn_simpl1 (T1lt_anti pa) (T1lt_ne' pa).
Qed.

Lemma T1lt_add2l p m n : (p + m < p + n) = (m < n).
Proof. by rewrite !T1ltNge T1le_add2l. Qed.

Lemma T1lt_add2r p m n : (m + p < n + p ) -> (m < n).
Proof.
elim: m p n.
by move => p n; rewrite T1add0n; case: n => //;rewrite T1add0n T1ltnn.
move => a Ha n b Hb; case; first by move => u; rewrite ! T1addn0.
move => a' n' b'; case.
simpl;case (T1ltgtP a a') => pa /=.
+ by rewrite !T1ltnn ltnn !if_same.
+ by rewrite (T1lt_anti pa) (T1lt_ne' pa).
+ by rewrite pa T1ltnn eqxx ltn_simpl1 eqn_simpl1.
move => a'' n'' b'' /=.
case (T1ltgtP a a'); case (T1ltgtP a a'') => pa pb //.
- by rewrite (T1lt_trans pa pb) T1ltnn.
- by rewrite -pa pb T1ltnn.
- case (T1ltgtP a'' a') => pc /=; rewrite ? pc.
+ by rewrite (T1lt_anti pb) (T1lt_ne' pb).
+ by rewrite (T1lt_anti pa) (T1lt_ne' pa).
+ by rewrite (T1lt_anti pb) (T1lt_ne' pb).
- rewrite - pa pb (T1lt_anti pb) /= T1ltnn eqxx.
by case (ltngtP n n'') => // _; apply: Hb.
- by rewrite - pb pa /= T1ltnn eqxx ltn_simpl1 eqn_simpl1.
- by rewrite -pa -pb /= !T1ltnn eqxx ltnS ltn_add2r if_same if_simpl=> ->.
Qed.

Lemma T1le_add2r p m n : (m <=n) -> (m + p <= n + p).
Proof. rewrite !T1leNgt; apply: contra; apply: T1lt_add2r. Qed.

Lemma T1eq_add2l p m n : (p + m == p + n) = (m == n).
Proof. by rewrite ! T1eq_le ! T1le_add2l. Qed.

Lemma add_le3 a b: a = a + b -> b = zero.
Proof. move /eqP;rewrite -{1} (T1addn0 a) T1eq_add2l => /eqP -> //. Qed.

Lemma add_le4 a b: b != zero -> a < a + b.
Proof.
move: (add_le1 a b); rewrite T1le_eqVlt.
by case: (a<a+b); rewrite ? orbT // orbF => /eqP /add_le3 ->.
Qed.

Lemma sub_pr1rCE (a := T1bad) (b := one) : (a - b == zero) && (b < a).
Proof. done. Qed.

## Limits

A limit ordinal is the supremum of a sequence of ordinals. We first show that some sequences are unbounded. We then show that, if the sequence is bounded, there is a least upper bound, more preciselly, if a property is satisfied for some NF ordinal, it is satisfied for a least NF aordinal. This requires teh excluded middel principle.

Fixpoint omega_tower (n:nat) : T1 :=
if n is p.+1 then phi0 (omega_tower p) else one.

Lemma omega_tower_nf n: T1nf (omega_tower n).
Proof. by elim: n ; [ | move => n H; rewrite /= andbT ]. Qed.

Lemma omega_tower_unbounded x: ~ (forall n, (omega_tower n) < x).
Proof.
elim :x; first by move => h; move: (h 0); rewrite T1ltn0.
move => a Ha n b _ c; case Ha => m.
move: (c m.+2); move /T1lt_cons_le;apply: T1lt_le_trans;apply: head_lt_cons.
Qed.

Definition ex_middle:=
forall (P: T1 -> Prop), let Q := exists x, (T1nf x /\ P x) in Q \/ ~Q.

Lemma ex_middle_pick (P: T1 -> Prop): ex_middle ->
(exists x, (T1nf x /\ P x)) \/ (forall x, T1nf x -> ~ (P x)).
Proof.
move => h.
by case (h P); [left |move => nq; right => x nx px; case nq; exists x ].
Qed.

Lemma min_exists (P: T1 -> Prop) x: ex_middle ->
T1nf x -> (P x) ->
exists y, T1nf y /\ P y /\ forall z, T1nf z -> P z -> y <= z.
Proof.
move => EM;move: x; apply: T1transfinite_induction.
move => x nx H px.
case (ex_middle_pick (fun z => (P z /\ ~ (x <= z))) EM).
move => [z [pa [pb pc]]].
have zx: z < x by rewrite (T1ltNge z x); apply /negP.
exact: (H _ pa zx pb).
move => qf.
exists x; split => //; split => // z pa pb; case xz: (x <= z) => //.
by case (qf _ pa); rewrite xz.
Qed.

### Definition

We say that x is the limit of f, or the supremum of the f(i) if f(i)<x (we could use less-or-equal here as f will be strictly increasing) and if moreover, every ordinal less than x is bounded by some f(i). Note that x is then the least upper bound. The trouble is that each f(i) may be NF and x is not. Thus , we give an alternate definition. Trouble is: a function may have more then one limit (at most one of them being NF).

Notation Tf := (nat -> T1).

Definition limit_v1 (f: Tf) x :=
(forall n, f n < x) /\ (forall y, y < x -> (exists n, y <= f n)).
Definition limit_v2 (f: Tf) x :=
(forall n, f n < x) /\ (forall y, T1nf y -> y < x -> (exists n, y <= f n)).

Lemma limit_unique1 (f: Tf) x x' :limit_v1 f x -> limit_v1 f x' ->
x = x'.
Proof.
move => [pa pb] [pc pd]; case: (T1ltgtP x x') => //.
by move /pd => [n]; rewrite T1leNgt (pa n).
by move /pb => [n]; rewrite T1leNgt (pc n).
Qed.

Lemma limit_unique2 (f: Tf) x x' : limit_v2 f x -> limit_v2 f x' ->
T1nf x -> T1nf x'-> x = x'.
Proof.
move => [pa pb] [pc pd] nx nx'; case: (T1ltgtP x x') => //.
by move /(pd _ nx) => [n]; rewrite T1leNgt (pa n).
by move /(pb _ nx') => [n]; rewrite T1leNgt (pc n).
Qed.

Definition omega_plus_n n := cons one 0 (cons zero n zero).

Lemma nf_omega_plus_n n : T1nf ( omega_plus_n n).
Proof. by []. Qed.

Lemma limit_CE1: limit_v1 omega_plus_n (cons one 0 T1omega).
Proof.
split; first by move => n.
move => y ;case: y => //; first by exists 0; rewrite T1le0n.
move => a n b /=; case: (T1ltgtP a one) => //.
by rewrite T1lt1 => /eqP -> _; exists 0.
move => ->; case: eqP => // ->; case: b => //; first by exists 0.
move => a' n' b' /=; rewrite /phi0 T1lt1 T1ltn0 !if_same if_simpl.
move /eqP ->; exists (n'.+1); rewrite T1le_consE T1ltnn !eqxx ltnn.
by rewrite T1le_consE T1ltnn !eqxx ltnSn.
Qed.

Lemma limit_CE2: limit_v2 omega_plus_n (cons one 1 zero).
Proof.
split; first by move => n.
move => y;case: y => //; first by exists 0; rewrite T1le0n.
move => a n b /=; case: (T1ltgtP a one) => //.
by rewrite T1lt1 => /eqP -> _ _; exists 0.
move => ->; rewrite T1ltn0 if_same if_simpl; case n => // /and3P [_ nb ltb] _.
move:nb ltb; case b => //; first by move => _ _; exists 0.
move => a' n' b' /and3P [_ _ ltb] /=.
rewrite T1lt1 T1ltn0 !if_same if_simpl => /eqP az.
move: ltb; rewrite az /phi0 T1lt1 => /eqP ->.
by exists n'; rewrite T1le_consE T1ltnn ltnn ! eqxx T1lenn.
Qed.

Lemma limit_CE3: limit_v2 omega_plus_n (cons one 0 T1omega).
Proof. by move: limit_CE1 => [sa sb]; split => // y _; apply: sb. Qed.

### The normal form

To each ordinal, one can associate another ordinal that is NF. However, this is in general incompatible with other operations

Fixpoint toNF x :=
if x is cons a n b then (cons (toNF a) n zero) + toNF b else zero.

Lemma nf_toNF x: T1nf (toNF x).
Proof.
by elim:x => //a Ha n b Hb; apply: nf_add => //=; rewrite -/toNF Ha.
Qed.

Lemma toNF_nz x : toNF x = zero -> x = zero.
Proof.
case x => // a n b /=; case (toNF b) => // a' n' b'.
by case (T1ltgtP (toNF a) a').
Qed.

Lemma toNF_nf x: T1nf x -> toNF x = x.
Proof.
elim:x => //a Ha n b Hb /and3P [/Ha sa /Hb sb etc].
by rewrite /toNF -/toNF sa sb add_to_cons.
Qed.

Lemma toNF_mon x : x <= toNF x.
Proof.
elim:x => //.
move => a Ha n b Hb /=; rewrite -/toNF.
have aux: if a < toNF a then true else if a == toNF a then true else false.
by case /orP: Ha => -> //; rewrite if_same.
move: Hb; case: (toNF b) => //.
by move => sa; rewrite T1le_consE ltnn eqxx sa aux.
move => a' n' b' sa; case: (T1ltgtP (toNF a) a') => sb.
+ by rewrite T1le_consE (T1le_lt_trans Ha sb).
+ by rewrite T1le_consE ltnn eqxx sa aux.
+ by rewrite T1le_consE ltnS leq_addr aux.
Qed.

Lemma toNF_ex1 x: toNF (cons zero 0 x) = one + toNF x.
Proof. by case: x. Qed.

Lemma toNF_ex2: toNF (cons one 0 T1omega) = cons one 1 zero.
Proof. by []. Qed.

Lemma toNF_succ (x := cons zero 0 one): toNF (T1succ x) != T1succ (toNF x).
Proof. by []. Qed.

Lemma toNF_pred (x := cons zero 0 one): toNF (T1pred x) != T1pred (toNF x).
Proof. by []. Qed.

### Realizing the limit

This is a simplification of the code given for the type T3 below. We define a function F(x); so that for any limit ordinal x, if f= F(x), then f is stictly increasing (of type nat -> T1), and its limit is x.

Lemma fincP (f: Tf) :
(forall n, f n < f n.+1) ->
(forall n m, (n < m)%N -> f n < f m).
Proof.
move => h n; elim => //.
move => m Hm;rewrite ltnS leq_eqVlt; case /orP;first by move => /eqP ->.
move /Hm => sa; exact: (T1lt_trans sa (h m)).
Qed.

Definition limit_of (f: Tf) x :=
[/\ (forall n m, (n < m)%N -> f n < f m), limit_v2 f x & T1nf x].

Lemma limit_unique f x y: limit_of f x -> limit_of f y -> x = y.
Proof. by move => [_ pa pb] [_ pc pd]; apply: (limit_unique2 pa pc pb pd). Qed.

Lemma limit_lub f x y: limit_of f x -> (forall n, f n <= y) -> T1nf y ->
x <= y.
Proof.
move => [pa [pb pc] pd ] hy; case (T1ltP y x) => // ha hb.
move: (pc _ hb ha) => [n ny].
by move: (T1le_lt_trans ny (pa _ _ (ltnSn n))); rewrite T1ltNge (hy n.+1).
Qed.

Definition phi1 a (f:Tf) := fun n => a + f n.
Definition phi2 (f:Tf) := fun n => phi0 (f n).
Definition phi3 a:= fun n => cons a n zero.

Lemma limit1 a b f: T1nf a -> limit_of f b -> limit_of (phi1 a f) (a + b).
Proof.
move => na [sa [sb sc] nb].
move: (nf_add na nb) => ns.
split => //; first by move => n m / sa => h; rewrite T1lt_add2l.
split; first by move => n; rewrite T1lt_add2l (sb n).
move => y ny hy.
case: (T1ltP a y) => cp; last first.
by exists 0; apply: (T1le_trans cp); rewrite add_le1.
move: (sub_pr1 ny (T1ltW cp)) => yv.
have ha: y - a < b by move: hy; rewrite {1} yv T1lt_add2l.
have [n nv] := (sc _ (nf_sub ny na) ha).
by exists n; rewrite yv T1le_add2l nv.
Qed.

Lemma limit2 b f: limit_of f b -> limit_of (phi2 f) (phi0 b).
Proof.
move => [sa [sb sc] nb]; rewrite /limit_of nf_phi0.
split => //; first by move => n m nm /=; rewrite (sa _ _ nm).
split => //; first by move => n; rewrite /= sb.
case => //; first by exists 0; rewrite T1le0n.
move => a' n' b' /and3P [na _ _] /=; rewrite T1ltn0 !if_same if_simpl => h.
move: (sc _ na h) => [n yn].
by exists n.+1; rewrite T1le_consE (T1le_lt_trans yn (sa _ _ (ltnSn n))).
Qed.

Lemma limit3 a: T1nf a -> limit_of (phi3 a) (phi0 (T1succ a)).
Proof.
move => na.
rewrite /limit_of nf_phi0 nf_succ //; split => //.
by move => n l nm /=; rewrite nm eqxx T1ltnn.
split; first by move => n; rewrite /= succ_lt.
case => //; first by exists 0; rewrite T1le0n.
move => a' n b /and3P [na' _ _] /=.
rewrite T1ltn0 !if_same if_simpl lt_succ_le_3 // T1le_eqVlt => aa.
by exists n.+1; move: aa; rewrite T1le_consE ltnSn; case (T1ltgtP a a').
Qed.

### Normal functions

We say that f:T2 -> T2 is a normal function if it is striclly increasing and the suppremum of all f(y), for y<x is f(x) whenever x is limit. Everything is assumed NF.

Fixpoint limit_fct x :=
if x is cons a n b then
if (b==zero) then
if(a==zero) then phi3 a
else if (T1is_succ a)
then if (n==0) then phi3 (T1pred a) else
phi1 (cons a n.-1 zero) (phi3 (T1pred a))
else if(n==0) then (phi2 (limit_fct a))
else phi1 (cons a n.-1 zero) (phi2 (limit_fct a))
else phi1 (cons a n zero) (limit_fct b)
else phi3 zero.

Lemma limit_prop x: T1nf x -> T1limit x -> limit_of (limit_fct x) x.
Proof.
elim:x => // a Ha n b Hb np /=.
move/and3P: np => [sa sb sc].
have nc: forall m, T1nf (cons a m zero) by move => m; rewrite /= andbT.
have Hc: forall m, (cons a m.+1 zero) = (cons a m zero) + phi0 a.
by move => m; rewrite /phi0 /= T1ltnn addn0.
case pa: (a==zero) => //; case bz: (b==zero); last first.
by move /(Hb sb) => sd; rewrite -(add_to_cons n sc); apply: limit1.
rewrite (eqP bz) => _.
case isa: (T1is_succ a).
have aux: (limit_of (phi3 (T1pred a)) (phi0 a)).
by rewrite {2} (succ_pred sa isa); apply: limit3; apply: nf_pred.
by case n => //= m; rewrite Hc; apply:limit1.
move: (limit_pr1 a); rewrite pa isa /= addbF => la.
have aux: (limit_of (phi2 (limit_fct a)) (phi0 a)) by apply: limit2; apply: Ha.
by case n => //= m; rewrite Hc; apply:limit1.
Qed.

Definition sup (f: T1-> T1) x z :=
[/\ T1nf z,
(forall y, T1nf y -> y < x -> f y <= z) &
(forall z', T1nf z' -> z' < z -> exists y,
[&& T1nf y, y < x & z' < f y])].

Definition normal f:=
[/\ forall x, T1nf x -> T1nf (f x),
(forall x y, T1nf x -> T1nf y -> x < y -> f x < f y)&
(forall x, T1nf x -> T1limit x -> sup f x (f x)) ].

Lemma sup_unique f x z z': sup f x z -> sup f x z' -> z = z'.
Proof.
move => [pa pb pc] [pa' pb' pc']; case (T1ltgtP z z') => //.
move/(pc' _ pa) => [y /and3P [qa qb qc]].
by move: (pb _ qa qb); rewrite T1leNgt qc.
move/(pc _ pa') => [y /and3P [qa qb qc]].
by move: (pb' _ qa qb); rewrite T1leNgt qc.
Qed.

Lemma sup_Oalpha_zero: sup id zero zero.
Proof.
by split; [ done | by move => y _; rewrite T1ltn0 | move => z; rewrite T1ltn0].
Qed.

Lemma sup_Oalpha_succ x: T1nf x -> sup id (T1succ x) x.
Proof.
move => nx;split.
- done.
- by move => y nf; rewrite lt_succ_le_3.
- by move => z nz zx; exists x => //; rewrite nx zx succ_lt.
Qed.

Lemma sup_Oalpha_limit x: T1nf x -> T1limit x -> sup id x x.
Proof.
move => nx lx ;split; [done | by move => y _ /T1ltW | ].
move => z nz zx; move: (limit_pr lx zx) => h.
by exists (T1succ z); rewrite h nf_succ // (succ_lt z).
Qed.

Identity is normal, composition of normal functions is normal, addition is normal when the firtst argument is fixed. A normal function maps limit ordinals to limit ordinls

Lemma normal_id: normal id.
Proof. split => //; apply: sup_Oalpha_limit. Qed.

Lemma normal_limit f x: normal f -> T1nf x -> T1limit x -> T1limit (f x).
Proof.
move => [pa pb pc] nx lx.
move: (pc _ nx lx) => [sa sb sc].
move: (limit_pr1 (f x)); case fz: (f x == zero).
have zx: zero < x by move: lx; case x.
have nz: T1nf zero by [].
by move: (pb zero x nz nx zx); rewrite (eqP fz) T1ltn0.
case: (T1limit (f x)) => //= sf.
move:(succ_pred (pa _ nx) sf) => eq1.
move: (sc _ (nf_pred sa) (pred_lt sf)) => [y /and3P [ny yx]].
by rewrite T1ltNge - (lt_succ_le_3 _ (pa _ ny)) - eq1 (pb _ _ ny nx yx).
Qed.

Proof.
move => na;split.
by move => x nx; apply: nf_add.
by move => x y nx ny; rewrite T1lt_add2l.
move => x nx lx; split.
by move => y _ /T1ltW; rewrite T1le_add2l.
move => z nz zp; case: (T1ltP z a) => az.
by exists zero; move: lx;rewrite T1addn0 az T1lt0n; case x.
move: (sub_pr1 nz az) => sa.
move:zp; rewrite {1} sa T1lt_add2l => sb.
exists (T1succ (z - a)).
by rewrite (nf_succ (nf_sub nz na)) (limit_pr lx sb) {1} sa T1lt_add2l succ_lt.
Qed.

Lemma normal_compose f g:
normal f -> normal g -> normal (f \o g).
Proof.
move => [pa pb pc][pa' pb' pc']; split.
- by move => x nx; apply: pa; apply: pa'.
- by move => x y nx ny h; apply: pb; [ apply: pa' | apply: pa' | apply: pb'].
- move => x nx lx.
move: (pa' _ nx) => ny.
have lg: T1limit (g x) by apply:normal_limit.
move:(pc _ ny lg) => [qa qb qc]; split => //.
move => y nu yx /=; apply:T1ltW;apply: pb; auto.
move: (pc' _ nx lx) => [qa' qb' qc'].
move => z' nz' h /=; move: (qc _ nz' h) => [y /and3P[ya yb yc]].
move: (qc' _ ya yb) => [z /and3P[za zb zc]]; exists z.
by rewrite za zb /=; apply: (T1lt_trans yc); apply: pb => //; apply: pa'.
Qed.

## multiplication

There is a unique way to define multiplication (for NF arguments) compatible with our interpretation of cons. In the case where a and a' are zero, we could use zero or b instead of b'. With the current implementation, multiplication is associative, and there is a distributivity law

Fixpoint T1mul (c1 c2 : T1) {struct c2}:T1 :=
if c2 is cons a' n' b' then
if c1 is cons a n b then
if((a==zero) && (a' == zero)) then cons zero (n*n' + n + n')%N b'
else if(a'==zero) then cons a (n*n' + n + n')%N b
else cons (a + a') n' ((cons a n b) * b')
else zero
else zero
where "c1 * c2" := (T1mul c1 c2) : cantor_scope.

Lemma mul_na n b x: (cons zero n b) * x = (cons zero n zero) * x.
Proof.
by elim: x => // a' _ n' b' Hb /=; rewrite Hb //;case pa: (a'==zero).
Qed.

Lemma T1muln0 x: x * zero = zero.
Proof. done. Qed.

Lemma T1mul0n x: zero * x = zero.
Proof. by case:x. Qed.

Lemma mul_int n m : \F n * \F m = \F (n *m)%N.
Proof.
case: n; first by rewrite T1mul0n.
move => n;case: m; first by rewrite T1muln0 muln0.
by move => m /=; rewrite - mulnE mulnSr addnC.
Qed.

Lemma mul_phi0 a b: phi0 (a + b) = phi0 a * phi0 b.
Proof.
simpl;case hb:(a== zero); case ha: (b==zero) => //=;rewrite (eqP ha) T1addn0 //.
rewrite (eqP hb) //.
Qed.

Lemma T1mul_eq0 x y: (x * y == zero) = (x== zero) || (y == zero).
Proof.
case: y x => [ [] |a n b] // [] // a' n' b' /=.
by case : (_ && _) => //; case: (a==zero).
Qed.

Lemma T1mul_eq1 a b: T1nf a -> (a* b == one) = ((a == one) && (b == one)).
Proof.
case: a => //; [ by rewrite T1mul0n | move => a' n' b'].
case: b => //; [ by rewrite T1muln0 andbF | move => a n b].
simpl; case pa: (a'== zero); last first.
case pb: (a==zero);rewrite !T1eqE pa // T1add_eq0 pa //.
case pb: (a== zero); last by rewrite andbF !T1eqE (T1add_eq0) pb ! andbF.
rewrite (eqP pa) T1lt1; move /and3P => [_ _ /eqP ->].
by rewrite /= !T1eqE pb /=; case n' => // m; case n => //=; rewrite muln0 addn0.
Qed.

Proof.
move => x y z; elim: y x z.
by move => x z; rewrite T1muln0 !T1add0n.
move => a _ n b Hb; case; first by move => z; rewrite ! T1mul0n.
move => a' n' b'; case; first by rewrite T1muln0 ! T1addn0.
move => a'' n'' b'' /=.
case ha: (a'==zero); [rewrite (eqP ha) !andTb | rewrite !andFb ].
case hb: (a==zero); first rewrite (eqP hb).
case hc: (a''==zero); last by move: hc; case a''.
case hc: (a'' == zero).
by rewrite T1lt0n hb /= hb Hb /=.
simpl;case pa: (a < a''); first by rewrite /= hc.
by case pb: (a'' < a); rewrite /= hb // Hb /= hc.
case: (altP (a=P zero)) => hb.
rewrite hb; case hc: (a''==zero).
by set X := (n' * n + n') %N;rewrite (addnAC (X + _)%N) (addnAC X).
by rewrite T1ltn0 T1lt0n hc /negb /= ha hc add_le4 // hc.
case hc: (a'' == zero).
have h: a' < a' + a by apply: add_le4.
rewrite (eqP hc) T1ltn0 T1lt0n hb /= ha /= h (T1lt_anti h) Hb //.
by rewrite (negbTE hb) /= ha.
by case (T1ltgtP a a''); rewrite /=? ha ? hc ?(negbTE hb)//= Hb /= ha hc.
Qed.

Lemma mulA: associative T1mul.
Proof.
move => x y z; elim: z y x; first by move => a b; rewrite !T1muln0.
move => a _ n b Hb; case; first by move => x; rewrite T1muln0 T1mul0n.
move => a' n' b';case; [by rewrite !T1mul0n | move => a'' n'' b'' /=].
have aux: (n'' * (n' * n + n' + n) + n'' + (n' * n + n' + n))%N =
((n'' * n' + n'' + n') * n + (n'' * n' + n'' + n') + n)%N.
rewrite ! mulnDl ! mulnDr mulnA ! addnA; congr (_ + _ + _)%N.
case pa: (a'==zero); first rewrite (eqP pa).
case pb: (a''== zero); rewrite ?(eqP pb) !andTb /= ? pb ? andFb.
case pc: (a==zero) => /=;[ by rewrite aux | by rewrite pc Hb /=].
case pc: (a==zero) => /=; rewrite pb andFb ? aux // pc Hb /= pb //.
case pb: (a==zero); rewrite /= ? pa ! andbF T1add_eq0 pa !andbF !andFb //.
by rewrite T1addA Hb /= pa andbF.
Qed.

Note that in some case the product of x and one is not x

Lemma T1muln1 x: T1nf x -> x * one = x.
Proof.
case: x => // a n b /= /and3P[_ _]; rewrite muln0 add0n addn0.
by case (altP (a =P zero)) => // ->; rewrite T1lt1 eqxx => /eqP ->.
Qed.

Lemma T1mul1n x: one * x = x.
Proof.
by elim: x => // a _ n b /= ->; case (altP (a =P zero)) => // ->.
Qed.

Lemma T1mul1nCE (x := T1bad): x * one <> x.
Proof. done. Qed.

Lemma T1muln1_CE x:
(x == x * one) =
(if x is cons a n b then ((a != zero) || (b== zero)) else true).
Proof.
by case: x => // a n b /=; rewrite muln0 addn0 fun_if !T1eqE !eqxx; case a.
Qed.

Lemma mul_succ x y: T1nf x -> x * (T1succ y) = x * y + x.
Proof. by move => h; rewrite succ_is_add_one mul_distr T1muln1. Qed.

Lemma T1lt_mul2l x y z: x != zero -> T1nf z -> ((x *y < x *z) = (y < z)).
Proof.
case x => // a n b _; elim: y z.
case;rewrite T1muln0 => // u v w //=; case a => //; case u => //.
move => a' Ha n' b' Hb; case; first by rewrite T1muln0 ! T1ltn0.
move => a'' n'' b'' nc.
move/and3P:(nc) => [_ nb _] /=.
case pa: (a==zero).
case pb: (a'==zero).
rewrite !andTb (eqP pb) (eqP pa); case a'' => //=.
by rewrite ltn_simpl2 eqn_simpl2.
case pc: (a''==zero); first by rewrite /= pb (eqP pc) T1ltn0 pb.
simpl;case pd:(a' < a'') => //; case pe:( a' == a'') => //.
case pf:( n'< n'')%N => //; case pg:( n' == n'')%N => //.
by move: (Hb _ nb); rewrite (eqP pa).
simpl.
case pb: (a'== zero).
case pc: (a'' == zero).
move: nc;rewrite (eqP pc) pb T1ltn0 T1nf_finite1=> /eqP ->.
by rewrite /= !T1ltnn T1ltn0 eqxx ltn_simpl2 eqn_simpl2 if_same if_simpl.
have: a < a + a'' by move: pc;rewrite -{1} (T1addn0 a) T1lt_add2l; case a''.
by rewrite (eqP pb) /= => ->; move: pc; case a''.
case pc: (a'' == zero).
case: (a' < a'') => //; case: (a' == a'') => //; case: (n' < n'')%N => //.
by case: (n' == n'')%N => //; apply: Hb.
Qed.

Lemma mulnf0 a n b: a != zero -> b < phi0 a -> (cons zero n zero) * b < phi0 a.
Proof.
case: b => // a' n' b'; rewrite phi0_lt1 /=.
by case pa: (a'==zero); [case a | rewrite phi0_lt1].
Qed.

Lemma nf_mul a b: T1nf a -> T1nf b -> T1nf (a * b).
Proof.
elim: b a => // => a Ha n b Hb; case => // a' n' b' sa.
case pb: (a==zero).
move: sa; rewrite /= (eqP pb) fun_if /= andbT;case eqP => // _ _ /andP [_].
rewrite /= pb andbF /=; move =>/and3P [na nb].
rewrite (nf_add (T1nf_consa sa) na) Hb //=.
case b; [ by rewrite T1muln0 /phi0 |move => u v w ].
rewrite /= ! (fun_if (fun z => z < phi0 (a' + a))) ! phi0_lt1.
by rewrite if_simpl => ->; rewrite andbF !if_same.
Qed.

Lemma T1lt_mul2r x y z: (y * x < z * x) -> (y < z).
Proof.
elim: x y z => // a Ha n b Hb.
case => //; [ case => // | move => a' n' b'; case].
by rewrite ! (fun_if (fun z => z < zero)) ! T1ltn0 !if_same.
move => a'' n'' b'' /=.
case pa: (a'==zero).
case pb: (a==zero).
rewrite (eqP pa) !andbT (eq_sym zero a'') T1lt0n;case a'' => //=.
by rewrite T1ltnn if_same if_simpl - ! mulnSr ltn_add2r ltn_mul2r /= => ->.
by case a''; rewrite (eqP pa) // !andbF /= !T1ltnn ltnn ! eqxx; move /Hb.
case pb: (a==zero).
case pc: (a''==zero); rewrite ! andbT /= ?pa? T1ltn0 //.
case (T1ltgtP a' a'') => //.
rewrite ! andbF /= ltnn eqxx.
case pc: (a' + a < a'' + a); first by rewrite (T1lt_add2r pc).
by case pd: (a' + a == a'' + a) => // /Hb.
Qed.

Lemma T1le_mul2l x y z : x != zero -> T1nf y ->
(x *y <= x *z) = (y <= z).
Proof. by move => sa sn; rewrite !T1leNgt T1lt_mul2l. Qed.

Lemma T1le_mul2r x y z: (y <= z) -> (y * x <= z * x).
Proof. by rewrite !T1leNgt; apply: contra; apply: T1lt_mul2r. Qed.

Lemma T1eq_mul2l p m n : p != zero -> T1nf m -> T1nf n ->
(p * m == p * n) = (m == n).
Proof. move => sa sb sc; rewrite ! T1eq_le ! T1le_mul2l => //. Qed.

Lemma T1le_pmulr x a: T1nf a -> x != zero -> a <= a * x.
Proof.
move => na xnz.
case az: (a==zero);first by rewrite (eqP az) T1mul0n.
by rewrite - {1} (T1muln1 na) T1le_mul2l ? az // T1ge1.
Qed.

Lemma T1le_pmulrCE (x:= \F1 ) (a:=T1bad) : (a <= a * x) = false.
Proof. done. Qed.

Lemma T1le_pmulrl x a: x != zero -> a <= x * a.
Proof.
move => xnz.
by rewrite - {1} (T1mul1n a); apply:T1le_mul2r; rewrite T1ge1.
Qed.

Lemma T1le_mulCE (m1:= one) (m2:= T1bad) (n1 := \F1) (n2 := one) :
(m1 <= n1) && (m2 <= n2) && ( m1 * m2 <= n1 * n2) == false.
Proof. done. Qed.

Lemma T1le_mul m1 m2 n1 n2 : T1nf m2 -> m1 <= n1 -> m2 <= n2 ->
m1 * m2 <= n1 * n2.
Proof.
move => nm2 s1 s2;apply (@T1le_trans (m1 * n2)).
case az: (m1==zero);first by rewrite (eqP az) ! T1mul0n.
by rewrite T1le_mul2l // az.
by apply:T1le_mul2r.
Qed.

### Preparation of the exponention

The prouct of an integer and omega is omega. This holds in fact for any limit ordinals. We give here a formula for the product of omega and x, and show that this is a limit ordinal. The converse holds.

Lemma mul_fin_omega n: (\F n.+1) * T1omega = T1omega.
Proof. done. Qed.

Lemma mul_int_limit n y: T1limit y -> \F n.+1 * y = y.
Proof.
elim y => // a _ m b Hb /=.
case pa: (a==zero) => //;case pb: (b==zero); last by move/Hb => ->.
by rewrite (eqP pb) T1muln0.
Qed.

Lemma T1mul_omega a n b:
T1omega * (cons a n b) =
if (a== zero) then cons one n zero else cons (one + a) n (T1omega * b).
Proof. by rewrite /T1omega/phi0 /=; case pa: (a==zero). Qed.

Lemma mul_omega_limit x: x != zero -> T1limit (T1omega * x).
Proof.
elim: x => // a _ n b Hb _.
rewrite T1mul_omega; case pa: (a==zero) => //.
rewrite /T1limit T1add_eq0 pa andbF -/T1limit.
case pb: (b== zero). by rewrite (eqP pb) T1muln0.
by rewrite (Hb (negbT pb)) orbT.
Qed.

Fixpoint T1div_by_omega x :=
if x is cons a n b then cons (a - one) n (T1div_by_omega b) else zero.

Lemma div_by_omega_pr x: T1nf x -> ((x==zero) || T1limit x)
-> T1omega * (T1div_by_omega x) = x.
Proof.
elim: x => // a _ n b Hb.
rewrite orFb /T1limit -/T1limit; case pa: (a==zero) => //.
move: (negbT pa); rewrite - T1ge1; case /orP.
move /eqP => <-.
rewrite /T1div_by_omega -/T1div_by_omega T1subnn T1mul_omega eqxx.
case b => // a' n' b' /=; move /andP => [_].
by rewrite T1lt1 T1ltn0 ! if_same if_simpl => ->.
move => lt1 /and3P [na /Hb h _] /h h'.
rewrite /T1div_by_omega -/T1div_by_omega T1mul_omega h'.
by rewrite - (sub1a (negbT pa) na) (negbTE (sub_nz na lt1)).
Qed.

We show here every ordinal x is the product of omega and y, to which an integer is added. We study the behaviour of this decomposition and multiplication

Lemma nf_div_by_omega x: T1limit x -> T1nf x -> T1nf (T1div_by_omega x).
Proof.
elim: x => // a _ n b Hb /= lx /and3P [sa sb sc]; apply /and3P; split => //.
+ by apply: nf_sub.
+ move: lx; case eqP => //_;case /orP; first by move /eqP -> .
by move => lb ; apply: Hb.
move: lx; case pa: (a==zero) => // h.
have oz: T1omega != zero by done.
have nz: T1nf (phi0 (a - cons zero 0 zero)) by rewrite nf_phi0 nf_sub //.
rewrite - (T1lt_mul2l (T1div_by_omega b) oz nz) div_by_omega_pr //.
by rewrite -[T1omega ]/(phi0 (one)) - mul_phi0 - sub1a // pa.
Qed.

Lemma nf_revCE u v: T1bad <> T1omega * u + \F v.
Proof.
case: (altP (u=Pzero)); first by move => ->; case v.
move/mul_omega_limit;set w:= (T1omega * u).
case: v; first by rewrite T1addn0 => sa sb; move: sa; rewrite - sb.
by move => v; case w => // a n b; case a.
Qed.

Lemma add_simpl3 x y: y != zero ->
x + x * (T1omega * y) = x * (T1omega * y).
Proof.
case: x => // a n b;case y => // a' n' b' _; rewrite T1mul_omega.
have e1: (one == zero) = false by done.
have e2: (one + a' == zero) = false by rewrite T1add_eq0 e1.
have e3: a < a + one by rewrite - succ_is_add_one succ_lt.
have e4: a < a + (one + a') by apply: add_le4; rewrite e2.
by case: eqP; rewrite /T1mul ? e1 ? e2 andbF -/T1mul {1}/T1add ? e3 ? e4.
Qed.

Lemma plus_int_Ox n x: x != zero -> \F n + T1omega * x = T1omega * x.
Proof.
case: n => // n xnz.
by move:(mul_omega_limit xnz); case (T1omega * x) => // a m b /=; case a.
Qed.

Lemma nf_rev x (u := (T1div_by_omega (T1split x).1)) (v:= (T1split x).2):
T1nf x -> T1nf u /\ x = T1omega * u + \F v.
Proof.
move => nx.
rewrite /u /v.
case (T1split x) => y n h ny. move: (h nx) => /andP [/eqP ->].
case /orP; first by move => /eqP -> //.
move => hh; move:(nf_div_by_omega hh ny) => sa /=.
by rewrite (div_by_omega_pr ny) //=; rewrite hh orbT.
Qed.

Lemma nf_rev_unique u v (x:= T1omega *u + \F v): T1nf u ->
u = T1div_by_omega (T1split x).1 /\ v = (T1split x).2.
Proof.
suff H: forall u v u' v', T1nf u -> T1nf u' ->
T1omega * u + \F v = T1omega * u' + \F v' -> u = u' /\ v = v'.
move => nu.
have nx: T1nf x by rewrite nf_add // ? nf_finite // nf_mul.
move: (nf_rev nx) => []; by apply: H.
clear x u v.
move => u v u' v' nu nu' h.
have aux1: forall a b, T1omega * a + \F b < T1omega * (T1succ a).
by move => a b; rewrite mul_succ // T1lt_add2l; case b.
have aux2: forall a b, T1omega * a <= T1omega * a + \F b.
move => a b; apply: add_le1.
move: (aux1 u v) (aux2 u' v'); rewrite h => sa sb.
move: (T1le_lt_trans sb sa); rewrite T1lt_mul2l // ?nf_succ // lt_succ_le_3 //.
move: (aux1 u' v') (aux2 u v); rewrite h => ta tb.
move: (T1le_lt_trans tb ta); rewrite T1lt_mul2l // ?nf_succ // lt_succ_le_3 //.
move => sc sd.
have uu': u = u' by move: sc sd; rewrite /T1le (eq_sym u'); case (T1ltgtP u u').
by move: h; rewrite uu' => /eqP; rewrite T1eq_add2l => /T1eqP /T1F_inj ->.
Qed.

Lemma nf_rev_sum x y
(u := T1div_by_omega (T1split x).1) (n:= (T1split x).2)
(v := T1div_by_omega (T1split y).1) (m:= (T1split y).2)
(w := T1div_by_omega (T1split (x+y)).1) (p:= (T1split (x+y)).2):
T1nf x -> T1nf y ->
if (v==zero) then (w = u /\ p = (n + m)%N) else (w = u+v /\ p = m).
Proof.
move => nu nv.
move: (nf_rev nu)(nf_rev nv); rewrite -/u -/v -/n -/m; move => [sa sb][sc sd].
case pa: (v==zero).
have eq3: x + y = T1omega *u + \F (n + m).
by move: (nf_rev_unique (n+m)%N sa); rewrite - eq3; move => [-> ->].
have eq3: x +y = T1omega * (u + v) + \F m.
by move: (nf_rev_unique m (nf_add sa sc)); rewrite - eq3; move => [-> ->].
Qed.

Lemma mul_sum_omega a n: a != zero ->
(T1omega * a + \F n) * T1omega = (T1omega * a) * T1omega.
Proof.
case: n; [ by rewrite T1addn0 | move => n].
elim: a => // a _ m b Hb _.
rewrite T1mul_omega; case pa: (a== zero) => //.
rewrite {2 4} /T1omega /phi0 /T1mul -/T1mul andbF //.
Qed.

Lemma nf_rev_prod x y
(u := T1div_by_omega (T1split x).1) (n:= (T1split x).2)
(v := T1div_by_omega (T1split y).1) (m:= (T1split y).2)
(w := T1div_by_omega (T1split (x*y)).1) (p:= (T1split (x*y)).2):
T1nf x -> T1nf y ->
if (u== zero)
then if (n == 0) then (w = zero /\ p = 0)
else (w = v /\ p = (n*m)%N)
else if (m==0) then (w = u * T1omega *v /\ p = 0)
else (w = u * T1omega *v + u * \F m /\ p = n).
Proof.
move => nu nv.
set H := nf_rev_unique.
move: (nf_rev nu)(nf_rev nv); rewrite -/u -/v -/n -/m; move => [sa sb][sc sd].
case pa: (u== zero).
have : x * y = (\F n) * T1omega * v + \F (n * m)%N.
by rewrite sb sd (eqP pa) T1muln0 T1add0n mul_distr mul_int mulA.
case n; first by rewrite /w /p /= T1mul0n T1add0n => ->.
move => n'; rewrite mul_fin_omega /= => h.
by move: h (H _ (n'.+1 * m)%N sc) => <- [-> ->].
move: (erefl (x* y)); rewrite {2} sd mul_distr mulA.
rewrite {2} sb mul_sum_omega ? pa // - !mulA => h.
have se: T1nf (u * (T1omega * v)) by rewrite !nf_mul //.
have sf: T1nf (u * (T1omega * v) + u * \F m).
by rewrite nf_add // nf_mul // nf_finite.
have aux: T1nf (T1omega * u) by rewrite nf_mul.
case pb: (m==0).
by move: h (H _ 0 se); rewrite (eqP pb) T1muln0; move => <- [-> ->].
have e1: \F n + x = x by rewrite sb T1addA plus_int_Ox ? pa //.
have e2: x * \F m = T1omega * u * \F m + \F n.
move: pb;elim m => // k Hr _; case ba: (k== 0).
by rewrite (eqP ba) T1muln1 // T1muln1.
by move: h (H _ n sf); rewrite e2 T1addA - mulA - mul_distr => <- [-> ->].
Qed.

### Normality of multiplication

If a is a non-zero ordinal, the multiplication by a is normal. This means, if b is limit, the supremum of all a *c for c<b is a*b. We show this for omega, and for some special cases. This is equivalent to existence of ordinal division.

Lemma mul_omega_pr1 a: a != zero -> T1nf a ->
sup (T1mul a) T1omega (a * T1omega).
Proof.
move => sa sb.
have sc: T1nf T1omega by [].
split; first by apply: nf_mul.
by move => y ny /T1ltW; rewrite (T1le_mul2l _ sa ny).
move => z nz zp.
move: sb sa zp; case: a => // a1 n1 b1 sb _; rewrite /= andbF.
move: nz; case z; first by exists one => //=; case: (_ && _).
move => a2 n2 b2 /= /and3P [ha hb hc].
rewrite T1ltn0 !if_same if_simpl - succ_is_add_one lt_succ_le_3 //.
case /orP => a12; last first.
exists one; simpl; move: a12; case az:(a1==zero); last by move => /= ->.
by rewrite (eqP az) T1ltn0.
rewrite (eqP a12).
exists (\F (n2.+2)); case az: (a1==zero).
Qed.

Lemma mul_omega2_pr1 a (u:= cons one 1 zero): a != zero -> T1nf a ->
sup (T1mul a) u (a * u).
Proof.
move => sa sb.
have sc: T1nf u by [].
split.
by apply: nf_mul.
by move => y ny /T1ltW; rewrite (T1le_mul2l _ sa ny).
move => z nz zp.
have eq1: a * u = a* T1omega + a * T1omega by rewrite - mul_distr //.
case: (T1ltP z (a* T1omega)) => zo; first by exists T1omega => //.
move: (sub_pr1 nz zo) => sd.
move: (mul_omega_pr1 sa sb) => [se _ sf].
move: zp; rewrite sd eq1; rewrite T1lt_add2l => sg.
move: (sf _ (nf_sub nz se) sg) => [y1 /and3P [ya yb yc]].
exists (T1omega + y1);
Qed.

Lemma mul_omega_pr3 a b c: a != zero -> c != zero ->
T1nf a -> T1nf b -> T1nf c ->
sup (T1mul a) c (a * c) ->
sup (T1mul a) (b+c) (a * (b + c)).
Proof.
move => az cz na nb nc [pa _ pc]; split => //.
by apply: nf_mul => //; apply: nf_add.
by move => y ny ybc; rewrite T1le_mul2l // T1ltW.
move => z nz zle.
case: (T1ltP z (a* b)) => zo.
by exists b; rewrite nb zo add_le4.
move: (sub_pr1 nz zo) => sd.
move: zle; rewrite sd mul_distr T1lt_add2l => se.
move: (pc _ (nf_sub nz (nf_mul na nb)) se) => [y1 /and3P [ya yb yc]].
by exists (b + y1); rewrite nf_add // mul_distr !T1lt_add2l yb yc.
Qed.

## Exponentiation

In order to compute a ^b , we first write b as the sum of a limit ordinal and an integer n. Computing a ^n is trivial. The limit ordinal is omega times c; if a is at least one, then a ^omega = omega ^d for some d, and the result is a ^ (omega * c) = omega ^(d*c)=phi0(d*c) . This leads to the following definitions.

Fixpoint exp_F a n :=
if n is p.+1 then a * (exp_F a p) else one.

Definition exp_O a b :=
if (a==zero) then if (b== zero) then one else a
else if (a== one) then one
else if (T1finite a) then (phi0 b)
else phi0 ((T1log a) * T1omega * b).

Definition T1exp a b:=
(exp_O a (T1div_by_omega (T1split b).1)) * (exp_F a ( (T1split b).2)).

Notation "a ^ b" := (T1exp a b) : cantor_scope.

Properties of exp_O

Lemma expO_mul1 a b: (exp_O a b) * (one) = exp_O a b.
Proof.
rewrite /exp_O; case: eqP; [by move => ->; case: eqP | case: eqP => //].
case:(T1finite a) => //=; rewrite andbT; case: eqP => // -> //.
Qed.

Lemma nf_expO a b: T1nf a -> T1nf b -> T1nf (exp_O a b).
Proof.
move => na nb; rewrite /exp_O; case: eqP => //; case: eqP => //.
by rewrite fun_if !nf_phi0 nf_mul ? nb // ?nf_mul // ? nf_log // if_same.
Qed.

Lemma expO_n0 x: exp_O x zero = one.
Proof. by rewrite /exp_O eqxx T1muln0 /= !if_same. Qed.

Lemma expO_1n n: exp_O (one) n = one.
Proof. done. Qed.

Lemma expO_eq0 a b: (exp_O a b == zero) = ((a== zero) && (b != zero)).
Proof.
rewrite /exp_O; case pa: (a==zero).
by rewrite (eqP pa); case pb: (b==zero).
by case: (a== one) => //; case :(T1finite a).
Qed.

Lemma expO_eq1 a b: (exp_O a b == one) = ((a== one) || (b == zero)).
Proof.
rewrite /exp_O.
case pb: (b==zero); first by rewrite (eqP pb) T1muln0 !if_same orbT.
rewrite orbF; case pa: (a==zero) => //;case pc: (a == one) => //.
rewrite (fun_if (fun z => z == one)) /phi0 /T1nat !T1eqE !andbT !T1mul_eq0 pb.
by case a => // a' n' b' /=; case (a'== zero).
Qed.

Lemma expO_add z u v: exp_O z u * exp_O z v = exp_O z (u + v).
Proof.
rewrite /exp_O; case: eqP.
move ->; case: eqP; first by move ->;rewrite T1mul1n //.
by move /eqP => uz;rewrite T1add_eq0 (negbTE uz) T1mul0n.
by case: eqP => //_ _;case (T1finite z); rewrite - mul_phi0 // mul_distr.
Qed.

Properties of exp_F
Lemma nf_expF a n: T1nf a -> T1nf (exp_F a n).
Proof. by move => na;elim: n => // n /= h; apply: nf_mul. Qed.

Lemma expF_add a n m: (exp_F a n) * (exp_F a m) = exp_F a (n + m).
Proof.
by elim: n; [ rewrite T1mul1n | move => n hr /=; rewrite - mulA hr].
Qed.

Lemma expF_mul a n m: exp_F a (n * m) = exp_F (exp_F a n) m.
Proof.
by elim: m; [ rewrite muln0 | move => m /= <-; rewrite expF_add mulnS ].
Qed.

Lemma expF_1n n: exp_F (one) n = one.
Proof. elim: n => // n /= -> //. Qed.

Lemma expF_eq0 a n: (exp_F a n == zero) = ((a== zero) && (n != 0)).
Proof.
elim: n => //; first by rewrite andbF.
by move => m /=; rewrite T1mul_eq0 => ->; rewrite andbC andKb andbT.
Qed.

Lemma expF_eq1 a n: T1nf a -> (exp_F a n == one) = ((a== one) || (n == 0)).
Proof.
move => na; elim: n => //; first by rewrite orbT.
by move => n h; rewrite /exp_F -/exp_F T1mul_eq1 // h ?orbF; case: eqP.
Qed.

Properties of exp

Lemma nf_exp a b: T1nf a -> T1nf b -> T1nf (a ^b).
Proof.
move => na nb.
move: (nf_split nb) (proj1 (nf_rev nb)) => sa sb.
rewrite /T1exp nf_mul // ?nf_expF // nf_expO //.
Qed.

Lemma exp00: zero ^zero = one.
Proof. done. Qed.

Lemma expx0 x: x ^zero = one.
Proof. by rewrite /T1exp expO_n0. Qed.

Lemma expx_pnat x n b: x ^ (cons zero n b) = exp_F x n.+1.
Proof. by rewrite /T1exp /T1split eqxx expO_n0 T1mul1n. Qed.

Lemma expx_nat x n: x ^ \F n = exp_F x n.
Proof. by case: n; [ rewrite expx0 | move => n; apply: expx_pnat]. Qed.

Lemma expx1 x: T1nf x -> x ^ one = x.
Proof. by move => h; rewrite /one expx_pnat /exp_F T1muln1. Qed.

Lemma expx1CE: T1bad ^ one = one.
Proof. done. Qed.

Lemma exp2omega n: (\F n.+2)^ T1omega = T1omega.
Proof. done. Qed.

Lemma exp1x x: one ^ x = one.
Proof. by rewrite /T1exp expO_1n expF_1n. Qed.

Lemma exp_eq0 x y: x^y == zero = ((x==zero) && (y != zero)).
Proof.
rewrite /T1exp T1mul_eq0 expO_eq0 expF_eq0.
rewrite - andb_orr; case pa: (x==zero) => //; rewrite !andTb.
by case y => // a n b /=; case pb: (a== zero) => //;case: (T1split b) => u v.
Qed.

Lemma exp0nz x: x != zero -> zero ^ x = zero.
Proof.
by move => h; move:(exp_eq0 zero x); rewrite h /= => /eqP.
Qed.

Lemma exp_eq1 x y: T1nf x -> T1nf y ->
(x^y == one) = ((x== one) || (y == zero)).
Proof.
move => nx ny; rewrite /T1exp;move: (nf_rev ny) => [sa sb].
rewrite [in RHS] sb T1mul_eq1 ? nf_expO // expF_eq1 // expO_eq1 T1add_eq0.
by rewrite T1mul_eq0 orFb; case pa: (x== one) => //=; case ((T1split y).2).
Qed.

Lemma exp_int a b: (\F a) ^ (\F b) = \F (a ^b%N).
Proof. by rewrite expx_nat; elim:b => // n h /=; rewrite h expnS mul_int. Qed.

Lemma exp_consCE1 (x := \F 2) (a := zero) (n := 0)(b := T1omega):
x ^(cons a n b) != x ^(cons a n zero) * x ^b.
Proof. done. Qed.

Lemma pow_omega x: T1nf x -> T1omega ^x = phi0 x.
Proof.
move => nx; rewrite {2} (proj2 (nf_rev nx)) /T1exp mul_phi0;congr T1mul.
by elim (T1split x).2 => // n /= -> ;rewrite /T1omega - mul_phi0; case n.
Qed.

### Existence and uniqueness of the Cantor Normal Form

Lemma cantor_exists a n b: T1nf (cons a n b) ->
cons a n b = (T1omega^a) * (\F n.+1) + b.
Proof.
have eq : cons a n zero = phi0 a * \F n.+1 by case a => //.
move =>/and3P [na _ sc]; rewrite - add_to_cons // eq; congr (_ * _ + _).
move: (proj2 (nf_rev na));set u := T1div_by_omega _;set v := (T1split a).2 => h.
rewrite /T1exp -/u -/v h mul_phi0; congr T1mul.
by elim v => // w /= <-; rewrite /T1omega - mul_phi0; case w.
Qed.

Lemma cantor_unique a n b a' n' b':
T1nf (cons a n b) -> T1nf (cons a' n' b') ->
(T1omega^a) * (\F n.+1) + b = (T1omega^a') * (\F n'.+1) + b' ->
(a=a' /\ n = n' /\ b = b').
Proof. by move => /cantor_exists <- /cantor_exists <-; case. Qed.