proposition: Lemma l_in_Dn : forall n, fst (Dn n) <= l <= snd (Dn n).
proof: Proof. intros n; split; apply le_epsilon; intros eps Heps; destruct (l_is_limit (eps / 2)) as [N H]. lra. destruct (sequence_bound n (Nat.max N n)) as [Hb _]. apply Nat.le_max_r. eapply Rle_trans; [apply Hb|]. apply Rabs_max. apply Rle_trans with (r2 := eps / 2); [|lra]. left; apply H; apply Nat.le_max_l. lra. destruct (sequence_bound n (Nat.max N n)) as [_ Hb]. apply Nat.le_max_r. assert (l - eps <= snd (Dn n)); [|lra]. eapply Rle_trans; [|apply Hb]. apply Rabs_min. apply Rle_trans with (r2 := eps / 2); [|lra]. left; rewrite Rabs_minus_sym; apply H. apply Nat.le_max_l. Qed.
imports: Reals Lra