proposition: Lemma diagonal_dist : forall n, R_dist (fst (Dn n)) (snd (Dn n)) <= (R_dist lb ub) * ((/2) ^ (S n)).
proof: Proof. intros n. induction n; simpl. replace ((R_dist lb ub) * (/2 * 1)) with ((R_dist lb ub) / 2) by field. apply succ_dist; exact not_empty. eapply Rle_trans. apply succ_dist; apply diagonal_compat. rewrite tech_pow_Rmult; replace (R_dist lb ub * (/2 * (/2) ^ (S n))) with (R_dist lb ub * (/ 2) ^ (S n) /2) by field; lra. Qed.
imports: Reals Lra