An exact proof term for the current goal is (R_lub_in_R (Romega_clipped_diffs f g) (Romega_uniform_metric_value f g) (Romega_uniform_metric_value_is_lub f g Hf Hg)).