proposition: Lemma BR_Cauchy_bounded s: CauchyQ s -> exists2 b, ratp b & forall n, natp n -> BQabs (Vg s n) <=q b.
proof: Proof. move => [pa pd]. have H: forall N, natp N -> exists2 b, ratp b & forall n, natp n -> n <c N -> BQabs (Vg s n) <=q b. apply:Nat_induction; first by exists \0q; [ apply:QS0 | move => n nn /clt0]. move => n nN [b bq Hrec]. have /QSa ha: inc (Vg s n) BQ by apply:BQ_seq_prop. case:(qleT_ee bq ha) => hb. exists (BQabs (Vg s n)) => // m mN /(cltSleP nN) lt. case: (equal_or_not m n) => emn; first by rewrite emn; BQo_tac. by apply:(qleT _ hb); apply: (Hrec _ mN). exists b => // m mN /(cltSleP nN) lt. by case: (equal_or_not m n) => emn; [rewrite emn | apply: (Hrec _ mN)]. move:(pd _ QpsS1) => [N NN Hb]. move:(H _ NN) => [b1 b1q b1p]. have ha: ratp (Vg s N) by apply:BQ_seq_prop. set b2:= (BQabs (Vg s N)) +q \1q. have b2q:= (QSs (QSa ha) QS1). have [b3 [b3q b1b3 b2b3]]: exists b3, [/\ inc b3 BQ, b1 <=q b3 & b2 <=q b3]. case:(qleT_ee b1q b2q) => h; [exists b2 | exists b1]; split=> //; BQo_tac. exists b3 => // n nN. case: (NleT_el NN nN); last by move => /(b1p _ nN) hc; BQo_tac. move => Nn. move: (Hb N n NN nN (cleR (CS_nat NN)) Nn) => hd. have he: ratp (Vg s n) by apply:BQ_seq_prop. move:(qle_triangular ha (QS_diff he ha)). rewrite (BQsum_diff ha he) (BQabs_diff he ha) => hf. move/(BQsum_lt2l (proj31_1 hd) (proj32_1 hd) (QSa ha)): hd => [hg _]. exact:(qleT (qleT hf hg) b2b3). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)