proposition: Lemma limit12b4 x y z: (limit12_hyp x (T3succ y) z) -> limit_of (phi12b4 x y z) [x,T3succ y,z].
proof: Proof. move => H0. set f := phi12b4 x y z. have ff:forall n m : nat, (n < m)%N -> f n < f 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 succ_lt 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 ny; rewrite psi_lt1. move: ny; 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 yb cz]. exists 1; rewrite T3le_consE T3lt_psi /lt_psi ax {3} (eqP yb) succ_lt. suff: ([a, b, c] < z) by move => ->; rewrite !orbT. move: H0 cz; case z => // a1 b1 c1 n1 d1 /=. move => /andP [/andP [/eqP -> /eqP ->]]; rewrite - (eqP yb) - (eqP ax). by case /orP => /andP[pa pb] pc; rewrite T3lt_psi /lt_psi pa pb pc !orbT. case /orP. move => /and3P [ax yb cz]. rewrite (lt_succ_le_3 _ nb) in yb. have [k kp] := (Hrec _ (leq_trans lc lm) nc cz). have ck1 := (T3le_lt_trans kp (ff _ _ (ltnSn k))). have ck2 := (T3lt_trans ck1 (ff _ _ (ltnSn k.+1))). exists k.+2; rewrite T3le_consE T3lt_psi /lt_psi ax ck1 ck2. by case /orP: yb => -> //;rewrite !orbT. case /orP. move => /and3P [ax bz cz]. exists 1; rewrite T3le_consE T3lt_psi /lt_psi ax (T3lt_trans (succ_lt y) bz). by case /orP: cz => ->; rewrite !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 ha: (b < f k) by apply /(T3le_lt_trans kp2) /ff; rewrite ltnS leq_addl. have hb: (c < f k) by apply /(T3le_lt_trans kp1) /ff; rewrite ltnS leq_addr. by exists k; rewrite T3le_consE T3lt_psi /lt_psi ax ha hb !orbT. rewrite - andb_orr orbC => /andP[xa xb]. exists 1. rewrite T3le_consE T3lt_psi /lt_psi xa (T3lt_anti xa) (T3lt_ne' xa)/=. case /orP: xb. by case/orP => ->; rewrite !orbT. rewrite succ_psi_lt2; first by case/orP => -> //;rewrite !orbT. by apply/negP;move /eqP => h; move: xa; case: h => ->; rewrite T3ltn0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)