proposition: Lemma limit5 f x: (limit_of f x) -> (limit_of (phi5 f) [x,zero,zero]).
proof: Proof. move => [sa sb sc]. have gi:forall n m : nat, (n < m)%N -> (phi5 f) n < (phi5 f) m. by move => n m /sa ha; rewrite T3lt_psi /lt_psi eqxx T3ltnn ha /= !orbT. split => //. by move => n; rewrite T3lt_psi /lt_psi eqxx T3ltnn (sb n) /= !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 ny; rewrite psi_lt1. have /and5P [_ lb lc _ _] := (size_prop1 a b c n d). rewrite T3lt_psi /lt_psi !T3ltn0 !andbF !orbF /=. move/and3P => [ ax bx cx]. move: ny; rewrite /T3nf -/T3nf => /and5P [na nb nc _ _]. have [n1 bp1] := (Hrec _ (leq_trans lb lm) nb bx). have [n2 cp1] := (Hrec _ (leq_trans lc lm) nc cx). have [n3 ap1] := (sc a na ax). set k := (n1 + n2 + n3).+1. have ha: (a < f k) by apply /(T3le_lt_trans ap1) /sa;rewrite ltnS leq_addl. have hb: (b < (phi5 f) k). by apply /(T3le_lt_trans bp1) /gi;rewrite /k ltnS -addnA leq_addr. have hc: (c < (phi5 f) k). by apply /(T3le_lt_trans cp1) /gi;rewrite /k ltnS addnAC leq_addl. exists k. by rewrite T3le_consE T3lt_psi /lt_psi !T3ltn0 !andbF !orbF /= ha hb hc. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)