proposition: Lemma middle_dist : R_dist x (middle x y) = (R_dist x y) / 2.
proof: Proof. unfold R_dist. rewrite middle_minus. unfold Rdiv. rewrite Rabs_mult. rewrite Rmult_eq_compat_l with (r2 := / 2). reflexivity. rewrite Rabs_Rinv. rewrite Rabs_pos_eq. reflexivity. lra. apply Rgt_not_eq; lra. Qed.
imports: Reals Lra