proposition: Lemma phiL x: T3nf x -> T3limit x -> limit_of (phi x) x.
proof: Proof. set n := (size x).+1. move: (leqnn n); rewrite {1}/n; move: n => n. elim: n x => [ // | k Hr]; case => //. move => a b c n d; rewrite ltnS => sa nx. move: (size_prop1 a b c n d) => /and5P[la lb lc ld le]. move: (nx); rewrite nf_consE => /and3P [nabc nd ne] lx. case dz: (d==zero); last first. move: lx => /=; rewrite dz /=; case:(all_zero a b c) => // ly. have py: limit_of (phi d) d by apply: Hr => //; apply: (leq_trans ld sa). have pd: T3nf(cons a b c n zero) by rewrite nf_consE nabc. rewrite phiE_2 ? dz // - (add_to_cons n ne); exact: (limit1 pd py). suff: limit_of (phi [a, b, c]) [a, b, c]. rewrite (eqP dz); case n => // m ha. have ny: T3nf (cons a b c m zero) by rewrite nf_consE nabc. by move: (limit1 ny ha); rewrite phiE_1 /T3add T3ltnn addn0. have la':= (leq_trans la sa). have lb':= (leq_trans lb sa). have lc':= (leq_trans lc sa). move: lx; rewrite /T3limit dz /= => lx. clear d la lb lc ld le sa nx nd dz ne. rewrite phiE_3 /phi_rec_psi. move: nabc; rewrite /T3nf -/T3nf =>/and5P[na nb nc _ _]. move: (limit_pr1 c). case cz: (c==zero). move: (limit_pr1 b). case bz: (b==zero). rewrite (eqP bz) (eqP cz). move: lx (limit_pr1 a); rewrite /all_zero bz cz. case az: (a==zero) => //=. case la: (T3is_succ a). move => _ _ _ _; rewrite {2} (succ_pred na la); apply: limit4. by rewrite addbF => _ lla _ _; apply: limit5; apply: Hr. case lb: (T3is_succ b). rewrite {3} (succ_pred nb lb) (eqP cz) => _ _; apply: limit6. by rewrite addbF => /= llb _; rewrite (eqP cz); apply: limit7;apply: Hr. case lc: (T3is_succ c). move: (limit_pr1 b). case bz: (b==zero). move: (limit_pr1 a). case az: (a==zero). rewrite (eqP az) (eqP bz) {3} (succ_pred nc lc) => _ _ _; apply: limit3. case la: (T3is_succ a). move => _ _ _; rewrite {2}(succ_pred na la) {2}(succ_pred nc lc)(eqP bz). apply: limit8. rewrite /= addbF (eqP bz) {3}(succ_pred nc lc)=> lla _ _. by apply: limit9; apply: Hr. case lb: (T3is_succ b). move => _ _. rewrite {2}(succ_pred nb lb) {2}(succ_pred nc lc). apply: limit10. rewrite /= addbF {3}(succ_pred nc lc) => lbb _; apply: limit11. by apply: Hr. rewrite /= addbF => lcc; move: (Hr _ lc' nc lcc) => hc. case h12: (limit12_hyp a b c); last by apply: limit12a => //; rewrite h12. move: (limit_pr1 b). case bz: (b==zero). move: (limit_pr1 a); move: h12. case az: (a==zero). by rewrite (eqP az) (eqP bz) => h12 _ _; apply:limit12b1. case la: (T3is_succ a). rewrite {1 4}(succ_pred na la) (eqP bz) => h12 _ _. by apply: limit12b2. rewrite /= addbF (eqP bz)=> h12 lla _. by apply: limit12b3 => //; apply: Hr. case lb: (T3is_succ b). by move: h12;rewrite {1 4}(succ_pred nb lb) => h12 _; apply: limit12b4. by rewrite /= addbF => llb; apply: limit12b5 => //; apply: Hr. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)