Let J, x, y and j be given.
Assume HJne: J ≠ Empty.
Assume Hx: x ∈ power_real J.
Assume Hy: y ∈ power_real J.
Assume HjJ: j ∈ J.
Assume H0: power_real_uniform_metric_value J x y = 0.
Set A to be the term power_real_clipped_diffs J x y.
Set l to be the term power_real_uniform_metric_value J x y.
Set a to be the term power_real_coord_clipped_diff x y j.
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 x y HJne Hx Hy).
We prove the intermediate claim Hcore: l ∈ R ∧ ∀b : set, b ∈ A → b ∈ R → Rle b l.
An exact proof term for the current goal is (andEL (l ∈ R ∧ ∀b : set, b ∈ A → b ∈ R → Rle b l) (∀u : set, u ∈ R → (∀b : set, b ∈ A → b ∈ R → Rle b u) → Rle l u) Hlub).
We prove the intermediate claim Hub: ∀b : set, b ∈ A → b ∈ R → Rle b l.
An exact proof term for the current goal is (andER (l ∈ R) (∀b : set, b ∈ A → b ∈ R → Rle b l) Hcore).
We prove the intermediate claim HaA: a ∈ A.
An exact proof term for the current goal is (ReplI J (λj0 : set ⇒ power_real_coord_clipped_diff x y j0) j HjJ).
We prove the intermediate claim HaR: a ∈ R.
An exact proof term for the current goal is (power_real_clipped_diffs_in_R J x y a Hx Hy HaA).
We prove the intermediate claim Hal: Rle a l.
An exact proof term for the current goal is (Hub a HaA HaR).
We prove the intermediate claim Hl0: l = 0.
We prove the intermediate claim HlEq: l = power_real_uniform_metric_value J x y.
Use reflexivity.
rewrite the current goal using HlEq (from left to right).
An exact proof term for the current goal is H0.
We prove the intermediate claim Ha0: Rle a 0.
rewrite the current goal using Hl0 (from right to left).
An exact proof term for the current goal is Hal.
We prove the intermediate claim HxjR: apply_fun x j ∈ R.
An exact proof term for the current goal is (power_real_coord_in_R J x j HjJ Hx).
We prove the intermediate claim HyjR: apply_fun y j ∈ R.
An exact proof term for the current goal is (power_real_coord_in_R J y j HjJ Hy).
We prove the intermediate claim Hdef: a = R_bounded_distance (apply_fun x j) (apply_fun y j).
An exact proof term for the current goal is (power_real_coord_clipped_diff_eq_R_bounded_distance J x y j HjJ Hx Hy).
We prove the intermediate claim HaNN: 0 ≤ a.
rewrite the current goal using Hdef (from left to right).
An exact proof term for the current goal is (R_bounded_distance_nonneg (apply_fun x j) (apply_fun y j) HxjR HyjR).
We prove the intermediate claim H0a: Rle 0 a.
An exact proof term for the current goal is (Rle_of_SNoLe 0 a real_0 HaR HaNN).
We prove the intermediate claim HaEq0: a = 0.
An exact proof term for the current goal is (Rle_antisym a 0 Ha0 H0a).
We prove the intermediate claim Hbd0: R_bounded_distance (apply_fun x j) (apply_fun y j) = 0.
rewrite the current goal using Hdef (from right to left).
An exact proof term for the current goal is HaEq0.
An exact proof term for the current goal is (R_bounded_distance_eq0 (apply_fun x j) (apply_fun y j) HxjR HyjR Hbd0).
∎