proposition: Lemma limit12b2 x y: (limit12_hyp (T3succ x) zero y) -> limit_of (phi12b2 x y) [T3succ x, zero, y].
proof: Proof. move => l12h. set f := phi12b2 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 =>//; first by apply: T3lt_psi_c. 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 sb. move: (T3lt_trans (succ_lt x) sa) => sc. exists 1. rewrite /= T3le_consE T3lt_psi /lt_psi sc (T3lt_anti sc) (T3lt_ne' sc) /=. by case /orP: sb => ->; rewrite !orbT. * case bz: (b==zero); last first. rewrite /= orbF => sa sb; move:(succ_lt x) => sc; exists 1. rewrite /= T3le_consE T3lt_psi /lt_psi sa sc (T3lt_anti sc) (T3lt_ne' sc). by rewrite - sa /=; case /orP: sb => ->; rewrite !orbT. rewrite /= orbF => sa sb. move:(succ_lt x) => sc; case: (T3leP [a, b, c] y) => sd. exists 1; case /orP: sd => xx; by rewrite /= T3le_consE T3lt_psi /lt_psi xx sa sc !orbT. move: sb sd l12h; case y => //. move => a1 b1 c1 n1 d1 /= ha hb /andP [/andP [/eqP nz /eqP dz]]. move: ha hb; rewrite nz dz => ha. rewrite T3lt_psi /lt_psi (eqP bz) (T3lt_anti ha) (T3lt_ne' ha) - sa. rewrite T3ltn0 !andbF !orbF !T3lt0n /= (eq_sym a). by case: (T3ltgtP a1 a) => //; case: (b1 == zero). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)