Let x, y, i and r be given.

Assume Hx: x ∈ R_omega_space.

Assume Hy: y ∈ R_omega_space.

Assume HiO: i ∈ ω.

Assume Hlt: Rlt (Romega_D_metric_value x y) r.

Set a to be the term mul_SNo (R_bounded_distance (apply_fun x i) (apply_fun y i)) (inv_nat (ordsucc i)).

We prove the intermediate claim Hale: Rle a (Romega_D_metric_value x y).

An exact proof term for the current goal is (Romega_D_metric_value_ub_scaled x y i Hx Hy HiO).

An exact proof term for the current goal is (Rle_Rlt_tra a (Romega_D_metric_value x y) r Hale Hlt).

∎