proposition: Lemma approx_min : forall (Un:nat -> R) (pr:has_lb Un) (eps:R), 0 < eps -> exists k : nat, Rabs (glb Un pr - Un k) < eps.
proof: Proof. intros Un pr. unfold glb. destruct lb_to_glb as (lb, Hlb). intros eps Heps. destruct (approx_maj _ pr eps Heps) as (n, Hn). exists n. unfold Rminus. rewrite <- Ropp_plus_distr, Rabs_Ropp. replace lb with (lub (opp_seq Un) pr). - now rewrite <- (Ropp_involutive (Un n)). - unfold lub. destruct ub_to_lub as (ub, Hub). apply Rle_antisym. + apply Hub. apply Hlb. + apply Hlb. apply Hub. Qed.
imports: Rbase Rfunctions Rseries Lia