Let x be given.

Assume Hx: x ∈ R_omega_space.

Set A to be the term Romega_D_scaled_diffs x x.

We prove the intermediate claim HAeq: A = {0}.

An exact proof term for the current goal is (Romega_D_scaled_diffs_diag_eq_Sing0 x Hx).

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

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

We prove the intermediate claim Hlub0: R_lub A 0.

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

An exact proof term for the current goal is R_lub_Sing0.

An exact proof term for the current goal is (R_lub_unique A (Romega_D_metric_value x x) 0 Hlub1 Hlub0).

∎