proposition: Lemma limit9 x y f: (limit_of f x) -> (limit_of (phi9 x y f) [x,zero, T3succ y]).
proof: Proof. move => [sa sb sc]. set g := (phi9 x y f). have ff:forall n m : nat, (n < m)%N -> g n < g m. by apply: fincP => n /=; apply: T3lt_psi_c. split => //. elim; first by rewrite T3lt_psi/lt_psi eqxx succ_lt. by move => n /= H; rewrite /= T3lt_psi /lt_psi H /= -/phi9 sb !orbT. move => t. move:{2} (size t).+1 (leqnn (size t).+1) => n; elim: n t=> //. move => m Hrec t; rewrite ltnS. case: t => //; first by move => _ _ _; exists 0; rewrite T3le0n. move => a b c n d lm nt; rewrite psi_lt1. move: nt; rewrite /T3nf -/T3nf => /and5P [na nb nc _ _]. move /and5P: (size_prop1 a b c n d) => [la lb lc ld _]. rewrite T3lt_psi' /lt_psi T3ltn0 T3len0 !andbF /=. case /orP. move /and3P => [ax lby cy]. rewrite (lt_succ_le_3 _ nc) in cy. exists 1; rewrite T3le_consE T3lt_psi/lt_psi (eqP ax) (sb 0) (eqP lby). case /orP: cy; first by move /eqP ->; rewrite eqxx !orbT. by rewrite T3lt_psi /lt_psi => ->; rewrite !eqxx /= !orbT. case /orP. move /and3P => [ax lby cy]; rewrite T3lt0n in lby. have ha: ([a, b, c] < [a, zero, y]). apply:(T3le_lt_trans _ (T3lt_psi_c a zero y)). by rewrite - succ_psi_lt2 ?cy // T3eqE (negbTE lby) !andbF. exists 1. by rewrite T3le_consE T3lt_psi/lt_psi -(eqP ax) ha (eqP ax) (sb 0) !orbT. case /orP. move /and3P => [ax bz cz]. have [k1 kp1] := (Hrec _ (leq_trans lc lm) nc cz). have [k2 kp2] := (Hrec _ (leq_trans lb lm) nb bz). have [k3 kp3] := (sc _ na ax). set k := (k1 + k2+k3).+1. have pa:(b < g k.+1). by apply/(T3le_lt_trans kp2) /ff; rewrite /k ltnS - addnS addnAC leq_addl. have pb:(c < g k.+1). by apply/(T3le_lt_trans kp1) /ff; rewrite /k ltnS - addnS - addnA leq_addr. have pc:(a < f k). by apply/(T3le_lt_trans kp3) /sa; rewrite ltnS leq_addl. by exists k.+1; rewrite T3le_consE T3lt_psi/lt_psi pa pb pc !orbT. move /andP => [ha hb]. have hc: ([a, b, c] < [x, zero, y]). apply:(T3le_lt_trans _ (T3lt_psi_c x zero y)). rewrite - succ_psi_lt2 ?cy //; apply /negP => h. by move: ha; case: (eqP h) => ->; rewrite T3ltn0. exists 1. by rewrite T3le_consE T3lt_psi/lt_psi (T3lt_trans (sb 0) ha) hc !orbT. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)