proposition: Lemma limit2 b f: limit_of f b -> limit_of (phi2 f) (phi0 b).
proof: Proof. move => [sa [sb sc] nb]; rewrite /limit_of nf_phi0. split => //; first by move => n m nm /=; rewrite (sa _ _ nm). split => //; first by move => n; rewrite /= sb. case => //; first by exists 0; rewrite T1le0n. move => a' n' b' /and3P [na _ _] /=; rewrite T1ltn0 !if_same if_simpl => h. move: (sc _ na h) => [n yn]. by exists n.+1; rewrite T1le_consE (T1le_lt_trans yn (sa _ _ (ltnSn n))). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)