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