proposition: Lemma normal_limit f x: normal f -> T1nf x -> T1limit x -> T1limit (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: T1nf zero by []. by move: (pb zero x nz nx zx); rewrite (eqP fz) T1ltn0. case: (T1limit (f x)) => //= sf. move:(succ_pred (pa _ nx) sf) => eq1. move: (sc _ (nf_pred sa) (pred_lt sf)) => [y /and3P [ny yx]]. by rewrite T1ltNge - (lt_succ_le_3 _ (pa _ ny)) - eq1 (pb _ _ ny nx yx). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)