Let J, f and g be given.
Assume Hf: f ∈ power_real J.
Assume Hg: g ∈ power_real J.
Apply (xm (J = Empty)) to the current goal.
Assume HJ0: J = Empty.
We prove the intermediate claim Hdef: power_real_uniform_metric_value J f g = If_i (J = Empty) 0 (Eps_i (λr : set ⇒ R_lub (power_real_clipped_diffs J f g) r)).
Use reflexivity.
rewrite the current goal using Hdef (from left to right).
rewrite the current goal using (If_i_1 (J = Empty) 0 (Eps_i (λr : set ⇒ R_lub (power_real_clipped_diffs J f g) r)) HJ0) (from left to right).
An exact proof term for the current goal is real_0.
Assume HJne: ¬ (J = Empty).
An exact proof term for the current goal is (R_lub_in_R (power_real_clipped_diffs J f g) (power_real_uniform_metric_value J f g) (power_real_uniform_metric_value_is_lub J f g HJne Hf Hg)).
∎