proposition: Lemma limit_unique2 (f: Tf) x x' : limit_v2 f x -> limit_v2 f x' -> T1nf x -> T1nf x'-> x = x'.
proof: Proof. move => [pa pb] [pc pd] nx nx'; case: (T1ltgtP x x') => //. by move /(pd _ nx) => [n]; rewrite T1leNgt (pa n). by move /(pb _ nx') => [n]; rewrite T1leNgt (pc n). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)