proposition: Lemma CauchyR_alt x: CauchyR x <-> (BR_seq x /\ forall e, inc e BRps -> exists2 N, natp N & forall n m, natp n -> natp m -> N <=c n -> N <=c m -> BRabs ((Vg x n) -r (Vg x m)) <r e).
proof: Proof. split; move => [pa pb]; split => //. move => e /BRcompare_zero [e' ra rb]. move: (pb _ ra) => [N NN h]; exists N => // n m nN mN na nb. move:(h _ _ nN mN na nb) => lt1; BRo_tac. move => e /BRcompare_zero' [e' ra rb]. move: (pb _ ra) => [N NN h]; exists N => // n m nN mN na nb. move:(h _ _ nN mN na nb) => lt1; BRo_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)