proposition: Lemma limit12b5 x y z f: (limit_of f y) -> (limit12_hyp x y z) -> (limit_of (phi12b5 x z f) [x,y,z]).
proof: Proof. move => [sa sb sc] H0. set g := (phi12b5 x z 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 eqxx /= -/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. case /orP. move /and3P => [ax lby cy]. exists 1; rewrite T3le_consE T3lt_psi/lt_psi ax (eqP lby)(sb 0) cy. suff: ([a, y, c] < z) by move => ->; rewrite !orbT. move: H0 cy; case z => // a1 b1 c1 n1 d1 /=. move => /andP [/andP [/eqP -> /eqP ->]] h; rewrite T3lt_psi' => ->. by case /orP:h => /andP[pa pb]; rewrite (eqP ax) pa ? pb !orbT. case /orP. move /and3P => [ax lby cy]. have [k1 kp1] := (Hrec _ (leq_trans lc lm) nc cy). have [k2 kp2] := (sc _ nb lby). set k := (k1 + k2).+1. have pa:(b < f k) by apply/(T3le_lt_trans kp2) /sa; rewrite ltnS leq_addl. have pb:(c < g k.+1). by apply/(T3le_lt_trans kp1) /ff; rewrite /k ltnS -addnS leq_addr. by exists k.+1; rewrite T3le_consE T3lt_psi/lt_psi ax pa pb !orbT. case /orP. move /and3P => [ax lby cy]. exists 1; rewrite T3le_consE T3lt_psi/lt_psi ax (T3lt_trans (sb 0) lby). 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). set k := (k1 + k2).+1. have pa:(b < g k) by apply/(T3le_lt_trans kp2) /ff; rewrite ltnS leq_addl. have pb:(c < g k) by apply/(T3le_lt_trans kp1) /ff; rewrite ltnS leq_addr. by exists k; rewrite T3le_consE T3lt_psi/lt_psi ax pa pb !orbT. case/orP;move /andP => [ax bx]. case (T3ltP z y) => yz; last first. exists 1; rewrite T3le_consE T3lt_psi/lt_psi ax. by case/orP: (T3le_trans bx yz) => ->; rewrite !orbT. move: H0 yz; case z => // a1 b1 c1 n1 d1 /=. move => /andP [/andP [/eqP -> /eqP ->]] pv pw; move: pv. rewrite (T3lt_anti (T3lt_trans (T3lt_psi_b a1 b1 c1) pw)). by rewrite (T3lt_anti pw) !andbF. exists 1. by rewrite T3le_consE T3lt_psi/lt_psi ax; case/orP: bx => ->; rewrite !orbT. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)