proposition: Lemma CauchyR_when_limit x: BR_seq x -> (exists2 y, realp y & limitR x y) -> CauchyR x.
proof: Proof. move => ha [y yq hb]; split => // e ep. have hep:=(BQhalf_pos ep). have heq:=(BQps_sBQ hep). move:(hb _ hep) => [N NN etc]; exists N => // n m nN mN na nb. move: (etc n nN na)(etc m mN nb) => sa sb. move:(BRsum_Mltlt sa sb). rewrite (BRsum_cQ heq heq). rewrite (BQdouble_half1 (BQps_sBQ ep))=> sc. have xnq: realp (Vg x n) by apply: BR_seq_prop. have xmq: realp (Vg x m) by apply:BR_seq_prop. move: (rle_triangular (RS_diff xnq yq) (RS_diff yq xmq)). rewrite (BRsumA (RS_diff xnq yq) yq (RSo xmq)) (BRsum_diff1 yq xnq). rewrite (BRabs_diff yq xmq) => sd; BRo_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)