proposition: Lemma BR_seq_of_Q_cauchy s: CauchyQ s -> CauchyR (BR_seq_of_Q s).
proof: Proof. move => [su sd]. move:(BR_seq_of_Q_seq su) => sa'. split => // e ep; move:(sd _ ep) => [N nN etc]; exists N => //n m na nb nc nd. rewrite /BR_seq_of_Q; move:(etc _ _ na nb nc nd); rewrite !LgV//. have ha: ratp (Vg s n) by apply: BQ_seq_prop. have hb: ratp (Vg s m) by apply: BQ_seq_prop. rewrite(BRdiff_cQ ha hb) (BRabs_cQ (QS_diff ha hb)) => h. by move/(rlt_cQ (proj31_1 h) (proj32_1 h)):h. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)