proposition: Lemma phi_mono_a a b b': T2nf b -> b < b' -> phi a b < phi a b'.
proof: Proof. move => nb bb'. have aux: forall u v, u < v -> [a, u] < [a, v]. by move => u v h; rewrite T2lt_psi /lt_psi eqxx h orbT. case:(phi_cases a b); last first. move =>[sa sb]; rewrite sa;case:(phi_cases a b'); last first. move => [ua ub]; rewrite ua; apply: aux. rewrite {1} sb in sa; rewrite {1} ub in ua. move: bb'; rewrite {1} sb {1} ub. move: (phi_inv1 sa) => [n [xa xb]]; rewrite xa. move: (phi_inv1 ua) => [m [ya yb]]; rewrite ya. set u1 := (T2_pr1 (T2pred b)); set u2 := (T2_pr2 (T2pred b)). set v1 := (T2_pr1 (T2pred b')); set v2 := (T2_pr2 (T2pred b')). simpl; rewrite T2lt_consE -T2lt_psi ltnn eqxx. case ta: ([u1,u2]==one). case tb: (cons v1 v2 O zero == one); first by rewrite T2ltnn. rewrite (eqP ta) T2gt1 tb //. case tb: (cons v1 v2 O zero == one). move: ta; rewrite T2lt_consE -T2lt_psi T2lt1 T2eqE !eqxx !andbT/=. by move => ->. rewrite T2lt_consE -T2lt_psi ltnn eqxx; case: ([u1, u2] < cons v1 v2 O zero) => //. case: ((u1 == v1) && (u2 == v2)) => //. case m => //;[ by case n | by move => m'; case n]. case => h; last first. rewrite h; apply: (T2lt_trans _ (aux _ _ bb')). by apply: aux; rewrite {2} sb; apply: succ_lt. move: (phi_fix2 h) => [sc sd]. by rewrite h sc T2lt_psi /lt_psi sd - sc (T2le_lt_trans (pred_le b) bb'). case; first by move => ->; exact:(T2lt_le_trans bb' (phi_ab_le1 a b')). move => sa; rewrite sa; case:(phi_cases a b'). case; last by move => ->; apply: aux. move => h; move: (phi_fix2 h) => [sc sd]; rewrite h sc. by rewrite T2lt_psi /lt_psi sd - sc bb'. move=> [sb sc]; rewrite sb; apply: aux. move: bb'; rewrite {1} sc lt_succ_le_3 //; case /orP => // /eqP h. move: sa; rewrite h. rewrite {1} sc in sb. move: (phi_inv1 sb) => [n [xa xb]]; rewrite xa /= xb /=. set u := (T2_pr1 (T2pred b')); set v := T2_pr2 (T2pred b'). simpl; case n => /=. by move => h1; move: (T2lt_psi_b a [u,v]); rewrite - h1 T2ltnn. by move => n1 []; case n1 => // n2 [] h2; move: (n_Sn n2); rewrite - h2. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)