proposition: Lemma T2toB_mon1 x y: T2nf x -> T2nf y -> x < y -> T2toB x <o T2toB y.
proof: Proof. have HS:forall a b, Spsi (T2toB a) (T2toB b) = T2toB [a, b]. move => a b. have ox :=(OS_Spsi (@OS_T2toB a) (@OS_T2toB b)). by rewrite /= succ_zero (oprod1r ox) (osum0r ox). set n := (size x + size y).+1. move: (leqnn n); rewrite {1}/n; move: n. move => n; elim: n x y; first by move => a b//;rewrite ltn0. move => m Hrec []. move=> y _ _ _; case:y => // a b n c _ /=. move: (@Cardinal.succ_nz (nat_to_B n)) => snz. move:(NS_succ (nat_to_B_Nat n)) => n1. move:(@OS_T2toB a)(@OS_T2toB b) (@OS_T2toB c) => oa ob oc. move: (OS_Spsi oa ob) => ozx. move:(OS_prod2 ozx (OS_nat n1)) => o2. apply: (ord_ne0_pos (OS_sum2 o2 oc)) => h. move: (proj1 (osum2_zero o2 oc h)). by move: (oprod2_nz ozx (OS_nat n1) (Spsi_nz oa ob) snz). move => a b n c; case => // a' b' n' c' sz /=. move: sz; rewrite ltnS => la. move => /and4P[na nb nc etc] /and4P[na' nb' nc' etc']. move:(@OS_T2toB a) (@OS_T2toB b) (@OS_T2toB c) => oa ob oc. move:(@OS_T2toB a') (@OS_T2toB b') (@OS_T2toB c') => oa' ob' oc'. set x := Spsi (T2toB a) (T2toB b). set x' := Spsi (T2toB a') (T2toB b'). have ox':=(OS_Spsi oa' ob'). have nN':=nat_to_B_Nat n'. have oxsn: ordinalp (x' *o csucc (nat_to_B n')). by apply:(OS_prod2 ox'); apply:OS_nat; apply:NS_succ. have l1: x' <=o x' *o csucc(nat_to_B n') +o T2toB c'. 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) oc'). apply: (osum_Mle0 ox' (OS_sum2 (OS_prod2 ox' on) oc')). move => leb. have lew1:= (T2le_cons_le (T2ltW leb)). move: (size_prop1 a b n c) => [pa pb pc pd]. move: (size_prop1 a' b' n' c') => [pa' pb' pc' pd']. have nab': T2nf [a', b'] by rewrite nf_psi na' nb'. have nab: T2nf [a, b] by rewrite nf_psi na nb. have HR: T2toB c <o x'. move: (T2lt_le_trans etc lew1);rewrite /x' HS; apply: Hrec => //. apply:leq_trans la; rewrite ltn_add_le //. move: leb;rewrite T2lt_consE /x'/x. case h1: (lt_psi a b a' b'); last first. case h2: ((a == a') && (b == b')) => //. rewrite /x;move/andP: h2 => [/eqP -> /eqP ->];rewrite -/x'. case:(ltngtP n n') => //; last first. move => -> cc; apply:(osum_Meqlt _ oxsn). move:cc; apply: Hrec=> //; apply:leq_trans la; rewrite ltn_add_le //. exact:(ltnW pc'). move => nn _; rewrite - (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). rewrite - (csum_Sn _ hc) - (osum2_2int hd he) (oprodD o1 o2 ox'). rewrite - (osumA (OS_prod2 ox' o1) (OS_prod2 ox' o2) oc'). rewrite -/x';set u := x' *o csucc (csucc (nat_to_B n)). have ou: ordinalp u by apply: OS_prod2 => //. have res1: x' *o csucc (nat_to_B n) +o T2toB c <o u. rewrite /u (succ_of_nat hc) (oprod2_succ ox' o3). by apply:(osum_Meqlt HR); apply: OS_prod2. apply:(olt_leT res1); apply:osum_Mle0 => //. by apply: OS_sum2 => //; apply:OS_prod2. move => _; apply:(olt_leT _ l1). suff: x <o x'. move => w3; apply: Spsi_indecomp_rec => //. have HR1: a' < a -> T2toB a' <o T2toB a. apply: Hrec => //; apply:leq_trans la. rewrite addnC ltn_add_le //; exact:(ltnW pa'). move:h1; case/orP; last first. move /andP => [/HR1 ha /eqP hb]. apply:(Spsi_cpc ob ha);rewrite HS hb; fprops. case /orP; last first. move => /andP [/HR1 ha hb]. have [Rb _]: T2toB [a,b] <o T2toB b'. apply: Hrec => //; apply:leq_trans la; rewrite ltn_add_el //. by apply:(Spsi_cpc ob ha); rewrite HS. case /orP; last first. rewrite /x/x';move /andP => [/eqP -> qb];apply:Spsi_cpb => //. apply:Hrec => //;apply:leq_trans la; rewrite ltn_add_le //; exact:(ltnW pb'). move => /andP [ha hb]. have hc:T2toB a <o T2toB a'. apply: Hrec => //; apply:leq_trans la;rewrite ltn_add_le //;exact:(ltnW pa'). apply: Spsi_cpa => //; rewrite HS; apply: Hrec => //. apply:leq_trans la; rewrite ltn_add_le //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)