proposition: Lemma R_cauchy_sequence_lower_bound: forall x:nat->R, cauchy R_metric x -> lower_bound (Im Full_set x).
proof: Proof. intros x Hx. pose proof (cauchy_impl_bounded R_metric R_metric_is_metric x Hx) as [p [r]]. clear Hx. exists (p - r). intros y Hy. apply H in Hy. clear H x. destruct Hy. unfold R_metric, Rabs in H. destruct (Rcase_abs _); lra. Qed.
imports: TopologicalSpaces OrderTopology MetricSpaces Coq(Lra Lia) ZornsLemma(EnsemblesTactics FiniteIntersections) RationalsInReals