proposition: Lemma cvg_at_rightNP {T : topologicalType} {R : numFieldType} (f : R -> T) a (l : T) : f @ a^'+ --> l <-> f \o -%R @ (- a)^'- --> l.
proof: Proof. by rewrite at_leftN -?fmap_comp; under [_ \o _]eq_fun => ? do rewrite /= opprK. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrint ssrnum finmap matrix) mathcomp(rat interval zmodp vector fieldext falgebra) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality set_interval Rstruct) ereal reals signed topology prodnormedzmodule