proposition: Lemma limit6 x y: limit_of (phi6 x y) [x,T3succ y, zero].
proof: Proof. set f := phi6 x y. 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 rewrite T3lt_psi /lt_psi eqxx !T3lt0n succ_lt /= orbT. by move => n /= H; rewrite /= T3lt_psi /lt_psi H succ_lt eqxx !orbT. move => z. move:{2} (size z).+1 (leqnn (size z).+1) => n; elim: n z=> //. move => m Hrec z; rewrite ltnS. case: z => //; 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 !T3ltn0 !andbF !orbF /=. rewrite (lt_succ_le_3 _ nb). case /orP. move /and3P =>[ax lby cz]. 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:lby => -> //; 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]. case abc1: ([a,b,c]== one). exists 1; rewrite T3le_consE T3lt_psi /lt_psi xa. rewrite (eqP abc1) (eq_sym one y); case: (T3ltgtP y one); rewrite ?orbT //. rewrite (T3lt_ne' xa) (T3lt_anti xa) /= T3lt1 => /eqP ->. rewrite T3lt_psi /lt_psi !T3lt0n T3eqE /= (eq_sym x). by case: (zero ==x) => //; rewrite eqxx !orbT. move: xb; rewrite -/(T3le _ _) succ_psi_lt2 ? abc1 // => xc. exists 1. by rewrite T3le_consE T3lt_psi /lt_psi xa; case /orP: xc => ->; rewrite !orbT. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)