proposition: Lemma CR_prop11 : realp (CR_limit f).
proof: Proof. apply/BR_P;split. - apply: Zo_S. - move:(CR_prop9 NS0) => xx; ex_tac. - move => h; move: QS0; rewrite / ratp - h => /Zo_P [_ [n nN / qgt0xP h2]]. case: (BQ_di_neg_pos h2). exact:(QpS_sum (CR_prop4 (NS_succ nN)) (BQps_sBQp (CR_prop0 nN))). - move => x y /Zo_P [ha [n hb hc]] lxy; apply /Zo_P; split. exact (proj32_1 lxy). by exists n => //; apply:(qlt_ltT hc lxy). move => x /Zo_P [ha [n hb hc]]. move:(BQmiddle_comp hc); set y := BQmiddle _ _; move => [qa qb]. by exists y => //; apply/Zo_P; split; [ exact: (proj31_1 qb) | exists n]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)