Let J, f and g be given.
Assume HJne: J ≠ Empty.
Assume Hf: f ∈ power_real J.
Assume Hg: g ∈ power_real J.
Set A to be the term power_real_clipped_diffs J f g.
We prove the intermediate claim HAnen: ∃a0 : set, a0 ∈ A.
An exact proof term for the current goal is (power_real_clipped_diffs_nonempty J f g HJne Hf Hg).
We prove the intermediate claim HAinR: ∀a : set, a ∈ A → a ∈ R.
Let a be given.
Assume HaA: a ∈ A.
An exact proof term for the current goal is (power_real_clipped_diffs_in_R J f g a Hf Hg HaA).
We prove the intermediate claim Hub1: ∀a : set, a ∈ A → a ∈ R → Rle a 1.
Let a be given.
Assume HaA: a ∈ A.
Assume _: a ∈ R.
Apply (ReplE_impred J (λj : set ⇒ power_real_coord_clipped_diff f g j) a HaA (Rle a 1)) to the current goal.
Let j be given.
Assume HjJ: j ∈ J.
Assume Haj: a = power_real_coord_clipped_diff f g j.
rewrite the current goal using Haj (from left to right).
An exact proof term for the current goal is (power_real_coord_clipped_diff_le_1 J f g j HjJ Hf Hg).
We prove the intermediate claim HubExists: ∃u : set, u ∈ R ∧ ∀a : set, a ∈ A → a ∈ R → Rle a u.
We use 1 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is real_1.
Let a be given.
Assume HaA: a ∈ A.
Assume HaR: a ∈ R.
An exact proof term for the current goal is (Hub1 a HaA HaR).
We prove the intermediate claim Hexlub: ∃l : set, R_lub A l.
An exact proof term for the current goal is (R_lub_exists A HAnen HAinR HubExists).
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 A r)).
Use reflexivity.
rewrite the current goal using Hdef (from left to right).
rewrite the current goal using (If_i_0 (J = Empty) 0 (Eps_i (λr : set ⇒ R_lub A r)) HJne) (from left to right).
An exact proof term for the current goal is (Eps_i_ex (λr : set ⇒ R_lub A r) Hexlub).
∎