proposition: Lemma limit1 a b f: T3nf a -> (limit_of f b) -> (limit_of (phi1 a f) (a + b)).
proof: Proof. move => na [sa sb sc]. split. + by move => n m / sa => h; rewrite T3lt_add2l. + by move => n; rewrite T3lt_add2l (sb n). + move => y ny hy. case: (T3ltP a y) => cp; last first. by exists 0; apply: (T3le_trans cp); rewrite add_le1. move: (sub_pr1 ny (T3ltW cp)) => yv. have ha: y - a < b by move: hy; rewrite {1} yv T3lt_add2l. have [n nv] := (sc _ (nf_sub ny na) ha). by exists n; rewrite yv T3le_add2l nv. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)