proposition: Lemma limit4 x: limit_of (phi4 x) [T3succ x, zero, zero].
proof: Proof. have ff:forall n m : nat, (n < m)%N -> phi4 x n < phi4 x m. by apply: fincP => n /=; apply: T3lt_psi_b. split => //. elim =>//. by rewrite /= T3lt_psi /lt_psi !T3lt0n /= succ_lt !orbT. by move => n /= H; rewrite /= T3lt_psi /lt_psi H succ_lt !orbT. move => y. move:{2} (size y).+1 (leqnn (size y).+1) => n; elim: n y=> //. move => m Hrec y; rewrite ltnS. case: y => //; first by move => _ _ _; exists 0; rewrite T3le0n. move => a b c n d lm. rewrite psi_lt1 /T3nf -/T3nf => /and5P [na nb nc _ _]. rewrite T3lt_psi /lt_psi !T3ltn0 /= !andbF !orbF /=. rewrite (lt_succ_le_3 _ na) => /and3P [asx bx cx]. have /and5P [la lb lc ld _] := (size_prop1 a b c n d). have [n1 bp1] := (Hrec _ (leq_trans lb lm) nb bx). have [n2 cp1] := (Hrec _ (leq_trans lc lm) nc cx). set k := (n1 + n2).+1. have ha: (b < phi4 x k) by apply:(T3le_lt_trans bp1); apply: ff; rewrite ltnS leq_addr. have hb: (b < phi4 x k.+1) by apply: (T3lt_trans ha); apply:ff. have hc: (c < phi4 x k.+1). by apply:(T3le_lt_trans cp1); apply: ff; rewrite ltnS /k -addSn leq_addl. exists k.+1. rewrite /= T3le_consE ltn0 T3len0 T3lt_psi /lt_psi ha hb hc. by case/orP: asx => ->; rewrite !orbT. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)