proposition: Lemma T1toB_mon1 x y: T1nf x -> T1nf y -> x < y -> T1toB x <o T1toB y.
proof: Proof. have qa: forall n u v, ordinalp n -> u <o omega0^o n ->v <o omega0^o n -> u +o v <o omega0^o n. move => n u v on ux vx; apply: (indecomp_prop2 ux vx (indecomp_prop4 on)). have qb: forall n u m, ordinalp n -> u <o omega0^o n -> natp m -> u *o m <o omega0^o n. move => n u m on ux nN; move:(proj31_1 ux) => ou. move: m nN; apply:Nat_induction. rewrite oprod0r; exact:(ole_ltT (ole0x ou) ux). move => m mN Hrec. rewrite (succ_of_nat mN) (oprod2_succ ou (OS_nat mN)). apply: (qa _ _ _ on Hrec ux). move => nx ny; move: (T1lenn y) ny (ny) nx. move: {2 3} (y) => z zy nz; move: z nz x y zy. apply:T1transfinite_induction. case; first by move => _ _ x y; rewrite T1len0 => /eqP ->; rewrite T1ltn0. move => za m zb nz Hrec. case. case => // a n b _ _ _ _ /=. move:(@OS_T1toB a)(@OS_T1toB b) => oa ob. move: (OS_pow OS_omega oa) => op. move: (@succ_nz (nat_to_B n)) => snz. move:(NS_succ (nat_to_B_Nat n)) => n1. move:(OS_prod2 op (OS_nat n1)) => o2. apply: (ord_ne0_pos (OS_sum2 o2 ob)) => h. move: (proj1 (osum2_zero o2 ob h)). by move: (oprod2_nz op (OS_nat n1) (oopow_nz oa) snz). move => a' n' b'; case => // a n b ha /=. move => /and3P [na nb etc] /and3P [na' nb' etc']. have ob := (@OS_T1toB b). have oa:=(@OS_T1toB a). have ox:= OS_pow OS_omega oa. set x := omega0 ^o T1toB a. have hb:=(T1lt_le_trans (head_lt_cons a n b) ha). have l1: x <=o x *o csucc(nat_to_B n) +o T1toB b. have nN:=nat_to_B_Nat n. have on := (OS_nat nN). rewrite (Nsucc_rw nN) csumC - (osum2_2int NS1 nN) (oprodD OS1 on ox). rewrite -/x (oprod1r ox) - (osumA ox (OS_prod2 ox on) ob). apply: (osum_Mle0 ox (OS_sum2 (OS_prod2 ox on) ob)). have rb: phi0 za <= cons za m zb. rewrite T1le_consE eqxx T1le0n T1ltnn; case m => //. have : a' <= a -> T1toB b' <o (omega0 ^o T1toB a'). move:nb' etc' ha. case: b'; first by move => _ _ _ _;apply:oopow_pos; apply:OS_T1toB. move => a'' n'' b'' nb''; rewrite phi0_lt1 /= => ha hc aa'. move: nb'' => /= /and3P [na'' nb'' etc'']. move: (T1le_lt_trans aa' hb) => ra. move: (Hrec a' na' ra a'' a' (T1lenn a') na' na'' ha) => l2. have nx:natp (csucc (nat_to_B n'')) by apply:NS_succ; apply:nat_to_B_Nat. have rc: phi0 a'' < cons za m zb. move:(T1lt_le_trans ha (T1le_trans aa' (T1le_cons_le hc))). rewrite -phi0_lt => rc; exact: (T1lt_le_trans rc rb). have l3: T1toB b'' <o omega0 ^o T1toB a''. move:na''; rewrite -nf_phi0 => nsa''. have op:= (OS_pow OS_omega (proj31_1 l2)). move: (Hrec _ nsa'' rc _ _ (T1lenn (phi0 a'')) nsa'' nb'' etc''). by rewrite /phi0 /= succ_zero (oprod1r op) (osum0r op). have l4:= (opow_Mo_lt l2). move: (olt_ltT l3 l4) => l5. apply: (qa _ _ _ (@OS_T1toB a') (qb _ _ _ (@OS_T1toB a') l4 nx) l5). case: (T1ltgtP a' a) => //. move => aa' HR _; apply:olt_leT l1. move: (Hrec a na hb a' a (T1lenn a) na na' aa') => /opow_Mo_lt l2. have ns: natp (csucc (nat_to_B n')) by apply:NS_succ; apply:nat_to_B_Nat. move: (HR (T1ltW aa')) => hr1. apply: qa; [exact oa | by apply: qb | exact: (olt_ltT hr1 l2)]. move => -> HR; case:(ltngtP n' n) => //. move => nn _; rewrite -/x - (subnKC nn) (nat_to_B_sum). have hc: natp (csucc (nat_to_B n')) by apply:NS_succ; apply:nat_to_B_Nat. have hd:= (NS_succ hc). have he: natp (nat_to_B (n - n'.+1)) by apply:nat_to_B_Nat. have o1 := (OS_nat hd). have o2 := (OS_nat he). have o3:= (OS_nat hc). set u := x *o csucc (csucc (nat_to_B n')). set v := (x *o nat_to_B (n - n'.+1) +o T1toB b). have ou := (OS_prod2 ox o1). have ov1:= (OS_prod2 ox o2). have hf:= (osum_Mle0 ou (OS_sum2 ov1 ob)). rewrite - nat_to_B_succ - (csum_Sn _ hc) - (osum2_2int hd he). rewrite (oprodD o1 o2 ox)- (osumA ou (OS_prod2 ox o2) ob). apply: (olt_leT _ hf). move:(osum_Meqlt (HR (T1lenn a)) (OS_prod2 ox o3)). by rewrite -(oprod2_succ ox o3) - (succ_of_nat hc). move => -> lbb. move:(T1le_cons_le ha); rewrite - phi0_le => h; move:(T1le_trans h rb) => rc. move:(Hrec b nb (T1lt_le_trans etc rc) b' b (T1lenn b) nb nb' lbb) => h2. apply:(osum_Meqlt h2); apply:(OS_prod2 ox (@OS_succN n)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)