proposition: Lemma decreasing_bounded_limit a xn (x := infimum BR_order (range xn)): BR_seq xn -> (forall n, natp n -> a <=r (Vg xn n)) -> (forall n, natp n -> Vg xn (csucc n) <=r Vg xn n) -> (a <=r x /\ limitR xn x).
proof: Proof. move => sa sb. move: (sa) => [sc sd se sf]. have ar :=(proj31(sb _ NS0)). move:BR_osr => [or sr]. have ha: sub (range xn) BR. move => t /(range_gP sc) [n na ->]; rewrite sd in na;exact:(proj32 (sb _ na)). have ha': sub (range xn) (substrate BR_order) by rewrite sr. have hb: nonempty (range xn). exists (Vg xn \0c); apply/(range_gP sc); rewrite sd. by exists \0c => //; apply: NS0. have hc: bounded_below BR_order (range xn). exists a; split; [ ue | move => y /(range_gP sc) [n na nb]]; apply /BR_gleP. by rewrite nb; apply:sb; rewrite /natp - sd. move: (infimum_pr1 or (BR_inf_exists ha hb hc)); rewrite -/x. move/(glbP or ha'); rewrite /lower_bound sr; move =>[[hd he] hf]. have ax: a <=r x. apply/BR_gleP; apply: hf; split => // y /(range_gP sc) [n na ->]. by rewrite sd in na; apply/BR_gleP; apply:sb. split; first exact. have aux: forall n, natp n -> BRabs (Vg xn n -r x) = (Vg xn n -r x). move => n nN. have : inc (Vg xn n) (range xn) by apply/(range_gP sc); exists n => //; ue. move/he => /BR_gleP le1. by apply: BRabs_pos; apply / rle0xP/ (rle_diffP1 hd (proj32 le1)). move => e ep. move:(RpsS_of_Q ep);set e' := BR_of_Q e => ep'. case: (p_or_not_p (exists2 y,inc y (range xn) & y <r (x +r e'))); last first. move: (BRsum_Mps hd ep') => l1 ne. have H: forall y, inc y (range xn) -> gle BR_order (x +r e') y. move => y yr; ex_middle t; case: ne; exists y => //. have yrr: realp y by rewrite / realp - sr; apply: ha'. by case:(rleT_el (proj32_1 l1) yrr) => // /BR_gleP. move/hf: (conj (proj32_1 l1) H) => /BR_gleP l2; BRo_tac. move => [y /(range_gP sc) [n nN ->] lt1]. rewrite sd in nN; exists n => // m mN lemn; rewrite (aux _ mN). have le1: Vg xn m <=r Vg xn n. rewrite - (cdiff_pr lemn);move: (m -c n) (NS_diff n mN). apply:Nat_induction; first by rewrite (Nsum0r nN); apply: rleR; BRo_tac. by move => k kN /(rleT (sf _ (NS_sum nN kN))); rewrite (csum_nS _ kN). apply /(BRsum_lt2l (RS_diff (proj31 le1) hd) (BRps_sBR ep') hd). rewrite (BRsum_diff hd (proj31 le1)); BRo_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)