Let f, g, i and r be given.

Assume Hf: f ∈ real_sequences.

Assume Hg: g ∈ real_sequences.

Assume Hi: i ∈ ω.

Assume Hlt: Rlt (Romega_uniform_metric_value f g) r.

We prove the intermediate claim Hle: Rle (Romega_coord_clipped_diff f g i) (Romega_uniform_metric_value f g).

An exact proof term for the current goal is (Romega_coord_clipped_diff_le_uniform f g i Hf Hg Hi).

An exact proof term for the current goal is (Rle_Rlt_tra_Euclid (Romega_coord_clipped_diff f g i) (Romega_uniform_metric_value f g) r Hle Hlt).

∎