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