Let x and y be given.

Assume Hx: x ∈ R_omega_space.

Assume Hy: y ∈ R_omega_space.

Set A to be the term Romega_D_scaled_diffs x y.

We prove the intermediate claim HAeq: A = Romega_D_scaled_diffs y x.

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

We prove the intermediate claim Hlub1: R_lub A (Romega_D_metric_value x y).

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

We prove the intermediate claim Hlub2': R_lub A (Romega_D_metric_value y x).

rewrite the current goal using HAeq (from left to right).

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

An exact proof term for the current goal is (R_lub_unique A (Romega_D_metric_value x y) (Romega_D_metric_value y x) Hlub1 Hlub2').

∎