proposition: Lemma BR_complete s: CauchyR s -> exists2 x, realp x & limitR s x.
proof: Proof. move => h. move:(limitR_same2 h) => [y ya yb]. move:(BR_complete1 ya) => [x xr xv]; exists x => //. move:(ya) => [yc _]. have ha: BR_seq s by move: h => []. have hb: BR_seq (BR_seq_of_Q y) by apply: BR_seq_of_Q_seq. exact: (limitR_same hb ha xr (similar_seq_sym ha hb yb) xv). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)