proposition: Lemma limit10 x y z: limit_of (phi10 x y z) [x,T3succ y, T3succ z].
proof: Proof. set f := phi10 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 rewrite T3lt_psi /lt_psi !eqxx succ_lt. 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. rewrite (lt_succ_le_3 _ nb) (lt_succ_le_3 _ nc). have ha:= (T3lt_psi_c x (T3succ y) z). case abc1: ([a,b,c] == one). case: (eqP abc1) => -> -> ->; exists 0. by rewrite T3le_consE T3gt1 /= /one T3eqE /= (negbTE(succ_nz y)) andbF. rewrite succ_psi_lt2 ? abc1 // succ_psi_lt2 ? abc1 //. case /orP. move => /and3P [ax lby cz]. exists 1. rewrite T3le_consE T3lt_psi /lt_psi ax (eqP ax) (eqP lby) succ_lt. case /orP: cz; first by move /eqP => ->; rewrite eqxx !orbT. by rewrite T3lt_psi /lt_psi !eqxx => ->; rewrite !orbT. 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 lby cz]. exists 1. rewrite T3le_consE T3lt_psi /lt_psi ax. by rewrite (T3le_lt_trans cz ha) (T3lt_trans (succ_lt y) lby) !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 hc: (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 hc 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 move => sa; rewrite (T3le_lt_trans sa ha) !orbT. by case /orP => -> //; rewrite !orbT. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)