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