proposition: Lemma normal_limit f x: normal f -> T3nf x -> T3limit x -> T3limit (f x).
proof: Proof. move => [pa pb pc] nx lx. move: (pc _ nx lx) => [sa sb sc]. move: (limit_pr1 (f x)); case fz: (f x == zero). have zx: zero < x by move: lx; case x. have nz: T3nf zero by []. by move: (pb zero x nz nx zx); rewrite (eqP fz) T3ltn0. case: (T3limit (f x)) => //= sf. have sd:T3pred (f x) < f x by rewrite {2} (succ_pred (pa _ nx) sf) succ_lt. move: (sc _ (nf_pred sa) sd) => [y /and3P[ny yx yc]]. move: yc; rewrite (lt_succ_le_4 _ (pa _ ny)). by rewrite -(succ_pred (pa _ nx) sf) T3leNgt (pb _ _ ny nx yx). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)