proposition: Lemma limit11 x y z f: (limit_of f y) -> (limit_of (phi11 x y z f) [x, y, T3succ z]).
proof: Proof. move => [sa sb sc]. set g := (phi11 x y 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 rewrite T3lt_psi/lt_psi !eqxx succ_lt. by move => n /= H; rewrite /= T3lt_psi /lt_psi H /= -/phi11 sb eqxx !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]. rewrite (lt_succ_le_3 _ nc) in cy. exists 1; rewrite T3le_consE T3lt_psi/lt_psi (eqP ax) (eqP lby) (sb 0). case /orP: cy; first by move /eqP ->; rewrite !eqxx !orbT. by rewrite T3lt_psi /lt_psi => ->; rewrite !eqxx /= !orbT. case /orP. move /and3P => [ax bz cz]. have [k1 kp1] := (Hrec _ (leq_trans lc lm) nc cz). have [k2 kp2] := (sc _ nb bz). 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 bz]; rewrite succ_psi_lt2 ?T3eqE ?(T3lcp0_pr bz) ?andbF //. by case/orP => h;exists 0; rewrite T3le_consE T3lt_psi/lt_psi ax bz h !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). 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 [xa yb]. exists 0. by rewrite T3le_consE T3lt_psi/lt_psi xa; case/orP: yb => ->;rewrite !orbT. exists 0; rewrite T3le_consE T3lt_psi/lt_psi xa. move: yb; rewrite succ_psi_lt2 ?T3eqE ?(T3lcp0_pr xa) ?andbF //. by case /orP => ->; rewrite !orbT. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)