proposition: Lemma R_dist_bounded_in_segment : forall a b c e, a <= b <= c -> R_dist a c < e -> R_dist b c < e.
proof: Proof. intros a b c e [ab bc] ace. unfold R_dist in *. assert (forall x y, x <= y -> Rabs (x - y) = y - x). intros. rewrite Rabs_minus_sym. apply Rabs_right. lra. pose proof (Rle_trans _ _ _ ab bc) as ac. repeat rewrite H; rewrite H in ace; intuition; apply Rle_lt_trans with (c - a); lra. Qed.
imports: Reals Rsequence_def Rsequence_facts Lia Lra