proposition: Lemma limit12b3 x y f: (limit_of f x) -> (limit12_hyp x zero y) -> (limit_of (phi12b3 y f) [x, zero, y]).
proof: Proof. move => [sa sb sc] H0. set g := (phi12b3 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 apply:T3lt_psi_c. by move => n /= H; rewrite /= T3lt_psi /lt_psi H /= -/phi11 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 !andbF !orFb. case /orP. move /and3P => [ax lby cy]. exists 1; rewrite T3le_consE T3lt_psi/lt_psi (eqP ax) (eqP lby)(sb 0). suff: ([x, zero, c] < y) by move => ->; rewrite !orbT. move: H0 cy; case y => // a1 b1 c1 n1 d1 /=. move => /andP [/andP [/eqP -> /eqP ->]] h; rewrite T3lt_psi' => ->. by case /orP:h => /andP[pa pb]; rewrite pa ? pb !orbT. case /orP. move /and3P => [ax lby cy]. exists 1; rewrite T3le_consE T3lt_psi/lt_psi (eqP ax) (sb 0) - (eqP ax). by case /orP: cy => ->; rewrite !orbT. case /orP. move /and3P => [ax lby cy]. have [k1 kp1] := (Hrec _ (leq_trans lc lm) nc cy). have [k2 kp2] := (Hrec _ (leq_trans lb lm) nb lby). 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 => [ax bx]. exists 1; rewrite T3le_consE T3lt_psi/lt_psi (T3lt_trans (sb 0) ax). by case /orP: bx => ->; rewrite !orbT. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)