proposition: Lemma succ_dist : R_dist (fst (succ x y k)) (snd (succ x y k)) <= (R_dist x y) / 2.
proof: Proof. unfold succ. destruct (total_order_T (middle x y) k) as [[_|_]|_]; simpl; [right|left|right]. apply middle_dist. repeat (rewrite middle_dist). apply epsilon_2. unfold Rdiv. apply Rmult_lt_0_compat; [|lra]. destruct (R_dist_pos x y) as [Hp|Hp]; [lra|]. apply -> R_dist_refl in Hp; lra. rewrite R_dist_sym; rewrite middle_sym. rewrite middle_dist. rewrite R_dist_sym; reflexivity. Qed.
imports: Reals Lra