Let f be given.
Assume Hf: f ∈ real_sequences.
Set A to be the term Romega_clipped_diffs f f.
We prove the intermediate claim HAeq: A = {0}.
An exact proof term for the current goal is (Romega_clipped_diffs_diag_eq_Sing0 f Hf).
We prove the intermediate claim Hlub1: R_lub A (Romega_uniform_metric_value f f).
An exact proof term for the current goal is (Romega_uniform_metric_value_is_lub f f Hf Hf).
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_uniform_metric_value f f) 0 Hlub1 Hlub0).
∎