proposition: Lemma limitR_alt x v : (limitR x v) <-> forall e, inc e BRps -> exists2 N, natp N & forall n, natp n -> N <=c n -> BRabs ((Vg x n) -r v) <r e.
proof: Proof. split. move => H e /BRcompare_zero [e' ra rb]. move:(H _ ra) => [N nN Hn]; exists N=> //n na nb; move:(Hn n na nb). move => lt; BRo_tac. move => H e /BRcompare_zero' [e' ra rb]. move:(H _ ra) => [N nN Hn]; exists N=> //n na nb; move:(Hn n na nb). move => lt; BRo_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)