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.
Assume Hl0: Rlt (power_real_uniform_metric_value J f g) 0.
We will prove False.
We prove the intermediate claim Hval0: power_real_uniform_metric_value J f g = 0.
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).
Use reflexivity.
We prove the intermediate claim Hl00: Rlt 0 0.
rewrite the current goal using Hval0 (from right to left) at position 1.
An exact proof term for the current goal is Hl0.
An exact proof term for the current goal is ((not_Rlt_refl 0 real_0) Hl00).
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.
Set l to be the term power_real_uniform_metric_value J f g.
We prove the intermediate claim Hlub: R_lub A l.
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 Hcore: l ∈ R ∧ ∀a : set, a ∈ A → a ∈ R → Rle a l.
An exact proof term for the current goal is (andEL (l ∈ R ∧ ∀a : set, a ∈ A → a ∈ R → Rle a l) (∀u : set, u ∈ R → (∀a : set, a ∈ A → a ∈ R → Rle a u) → Rle l u) Hlub).
We prove the intermediate claim Hub: ∀a : set, a ∈ A → a ∈ R → Rle a l.
An exact proof term for the current goal is (andER (l ∈ R) (∀a : set, a ∈ A → a ∈ R → Rle a l) Hcore).
Assume Hl0: Rlt l 0.
We will prove False.
Apply (power_real_clipped_diffs_nonempty J f g HJne2 Hf Hg) to the current goal.
Let a0 be given.
Assume Ha0A: a0 ∈ A.
We prove the intermediate claim Ha0R: a0 ∈ R.
An exact proof term for the current goal is (power_real_clipped_diffs_in_R J f g a0 Hf Hg Ha0A).
We prove the intermediate claim Ha0le: Rle a0 l.
An exact proof term for the current goal is (Hub a0 Ha0A Ha0R).
We prove the intermediate claim Ha0lt0: Rlt a0 0.
An exact proof term for the current goal is (Rle_Rlt_tra_Euclid a0 l 0 Ha0le Hl0).
Apply (ReplE_impred J (λj : set ⇒ power_real_coord_clipped_diff f g j) a0 Ha0A False) to the current goal.
Let j be given.
Assume HjJ: j ∈ J.
Assume Ha0eq: a0 = power_real_coord_clipped_diff f g j.
We prove the intermediate claim HfjR: apply_fun f j ∈ R.
An exact proof term for the current goal is (power_real_coord_in_R J f j HjJ Hf).
We prove the intermediate claim HgjR: apply_fun g j ∈ R.
An exact proof term for the current goal is (power_real_coord_in_R J g j HjJ Hg).
We prove the intermediate claim Hbd: a0 = R_bounded_distance (apply_fun f j) (apply_fun g j).
rewrite the current goal using Ha0eq (from left to right).
An exact proof term for the current goal is (power_real_coord_clipped_diff_eq_R_bounded_distance J f g j HjJ Hf Hg).
We prove the intermediate claim Hbdlt0: Rlt (R_bounded_distance (apply_fun f j) (apply_fun g j)) 0.
rewrite the current goal using Hbd (from right to left).
An exact proof term for the current goal is Ha0lt0.
We prove the intermediate claim HdR: R_bounded_distance (apply_fun f j) (apply_fun g j) ∈ R.
An exact proof term for the current goal is (R_bounded_distance_in_R (apply_fun f j) (apply_fun g j) HfjR HgjR).
We prove the intermediate claim HdS: SNo (R_bounded_distance (apply_fun f j) (apply_fun g j)).
An exact proof term for the current goal is (real_SNo (R_bounded_distance (apply_fun f j) (apply_fun g j)) HdR).
We prove the intermediate claim HbdNN: 0 ≤ R_bounded_distance (apply_fun f j) (apply_fun g j).
An exact proof term for the current goal is (R_bounded_distance_nonneg (apply_fun f j) (apply_fun g j) HfjR HgjR).
We prove the intermediate claim HbdltS: R_bounded_distance (apply_fun f j) (apply_fun g j) < 0.
An exact proof term for the current goal is (RltE_lt (R_bounded_distance (apply_fun f j) (apply_fun g j)) 0 Hbdlt0).
We prove the intermediate claim H00lt: 0 < 0.
An exact proof term for the current goal is (SNoLeLt_tra 0 (R_bounded_distance (apply_fun f j) (apply_fun g j)) 0 SNo_0 HdS SNo_0 HbdNN HbdltS).
An exact proof term for the current goal is ((SNoLt_irref 0) H00lt).
∎