Let f and g be given.
Assume Hf: f ∈ real_sequences.
Assume Hg: g ∈ real_sequences.
Set A to be the term Romega_clipped_diffs f g.
We prove the intermediate claim HAeq: A = Romega_clipped_diffs g f.
An exact proof term for the current goal is (Romega_clipped_diffs_sym f g Hf Hg).
We prove the intermediate claim Hlub1: R_lub A (Romega_uniform_metric_value f g).
An exact proof term for the current goal is (Romega_uniform_metric_value_is_lub f g Hf Hg).
We prove the intermediate claim Hlub2': R_lub A (Romega_uniform_metric_value g f).
rewrite the current goal using HAeq (from left to right).
An exact proof term for the current goal is (Romega_uniform_metric_value_is_lub g f Hg Hf).
An exact proof term for the current goal is (R_lub_unique A (Romega_uniform_metric_value f g) (Romega_uniform_metric_value g f) Hlub1 Hlub2').
∎