proposition: Lemma limit8 x y: limit_of (phi8 x y) [T3succ x, zero, T3succ y].
proof: Proof. set f := phi8 x y. have ff:forall n m : nat, (n < m)%N -> f n < f m. by apply: fincP => n /=; apply: T3lt_psi_b. split => //. elim =>//. by rewrite /= T3lt_psi /lt_psi !T3lt0n /= succ_lt !eqxx. by move => n /= H; rewrite /= T3lt_psi /lt_psi H succ_lt !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 !T3lt0n!andbF /=. case: (T3ltgtP a (T3succ x)). + rewrite /= orbF (lt_succ_le_3 _ na) => ax /andP [bx cx]. have [n1 bp1] := (Hrec _ (leq_trans lb lm) nb bx). have [n2 cp1] := (Hrec _ (leq_trans lc lm) nc cx). set k := (n1 + n2).+1. have ha: (b < f k) by apply:(T3le_lt_trans bp1); apply: ff; rewrite ltnS leq_addr. have hb: (b < f k.+1) by apply: (T3lt_trans ha); apply:ff. have hc: (c < f k.+1). by apply:(T3le_lt_trans cp1); apply: ff; rewrite ltnS /k -addSn leq_addl. exists k.+1. rewrite /= T3le_consE ltn0 T3len0 T3lt_psi /lt_psi ha hb hc. by case/orP: ax => ->; rewrite !orbT. + rewrite /= orbC -/(T3le _ _) => sa; rewrite succ_psi_lt2. by move => sb;exists 0; rewrite /= T3le_consE T3lt_psi' sa sb !orbT. apply /eqP => h; by move: sa; case: h => ->; rewrite T3ltn0. + case bz: (b==zero). * rewrite /= orbF (lt_succ_le_3 _ nc) => ax; case /orP. move => cy; move: (succ_lt x) => h. exists 1; rewrite /= T3le_consE T3lt_psi /lt_psi ax h (T3lt_anti h). by rewrite (T3lt_ne' h) /= (eqP bz) (eqP cy) eqxx !orbT. by exists 0; rewrite /= T3le_consE T3lt_psi /lt_psi ax bz T3ltnn eqxx b0. * rewrite /= orbF orbC -/(T3le _ _) => sa sb. exists 0. rewrite /= T3le_consE T3lt_psi /lt_psi T3ltn0 T3lt0n sa bz eqxx T3ltnn. by rewrite /= -sa orbF orbC -/(T3le _ _) -succ_psi_lt2 ? sb // T3eqE bz andbF. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)