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 Hdef1: 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.
We prove the intermediate claim Hdef2: power_real_uniform_metric_value J g f = If_i (J = Empty) 0 (Eps_i (λr : set ⇒ R_lub (power_real_clipped_diffs J g f) r)).
Use reflexivity.
rewrite the current goal using Hdef1 (from left to right).
rewrite the current goal using Hdef2 (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).
rewrite the current goal using (If_i_1 (J = Empty) 0 (Eps_i (λr : set ⇒ R_lub (power_real_clipped_diffs J g f) r)) HJ0) (from left to right).
Use reflexivity.
Assume HJne: ¬ (J = Empty).
We prove the intermediate claim HJne2: J ≠ Empty.
An exact proof term for the current goal is HJne.
Set A to be the term power_real_clipped_diffs J f g.
We prove the intermediate claim HAeq: A = power_real_clipped_diffs J g f.
An exact proof term for the current goal is (power_real_clipped_diffs_sym J f g Hf Hg).
We prove the intermediate claim Hlub1: R_lub A (power_real_uniform_metric_value J f g).
An exact proof term for the current goal is (power_real_uniform_metric_value_is_lub J f g HJne2 Hf Hg).
We prove the intermediate claim Hlub2': R_lub A (power_real_uniform_metric_value J g f).
rewrite the current goal using HAeq (from left to right).
An exact proof term for the current goal is (power_real_uniform_metric_value_is_lub J g f HJne2 Hg Hf).
An exact proof term for the current goal is (R_lub_unique A (power_real_uniform_metric_value J f g) (power_real_uniform_metric_value J g f) Hlub1 Hlub2').
∎