Let J, x, y and z be given.
Assume Hx: x ∈ power_real J.
Assume Hy: y ∈ power_real J.
Assume Hz: z ∈ power_real J.
Apply (xm (J = Empty)) to the current goal.
Assume HJ0: J = Empty.
Assume Hlt: Rlt (add_SNo (power_real_uniform_metric_value J x y) (power_real_uniform_metric_value J y z)) (power_real_uniform_metric_value J x z).
We will prove False.
We prove the intermediate claim Hxy0: power_real_uniform_metric_value J x y = 0.
We prove the intermediate claim Hdef: power_real_uniform_metric_value J x y = If_i (J = Empty) 0 (Eps_i (λr : set ⇒ R_lub (power_real_clipped_diffs J x y) 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 x y) r)) HJ0) (from left to right).
Use reflexivity.
We prove the intermediate claim Hyz0: power_real_uniform_metric_value J y z = 0.
We prove the intermediate claim Hdef: power_real_uniform_metric_value J y z = If_i (J = Empty) 0 (Eps_i (λr : set ⇒ R_lub (power_real_clipped_diffs J y z) 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 y z) r)) HJ0) (from left to right).
Use reflexivity.
We prove the intermediate claim Hxz0: power_real_uniform_metric_value J x z = 0.
We prove the intermediate claim Hdef: power_real_uniform_metric_value J x z = If_i (J = Empty) 0 (Eps_i (λr : set ⇒ R_lub (power_real_clipped_diffs J x z) 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 x z) r)) HJ0) (from left to right).
Use reflexivity.
We prove the intermediate claim Hsum0: add_SNo (power_real_uniform_metric_value J x y) (power_real_uniform_metric_value J y z) = 0.
rewrite the current goal using Hxy0 (from left to right).
rewrite the current goal using Hyz0 (from left to right).
An exact proof term for the current goal is (add_SNo_0R 0 SNo_0).
We prove the intermediate claim Hlt00: Rlt 0 0.
rewrite the current goal using Hsum0 (from right to left) at position 1.
rewrite the current goal using Hxz0 (from right to left) at position 1.
An exact proof term for the current goal is Hlt.
An exact proof term for the current goal is ((not_Rlt_refl 0 real_0) Hlt00).
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 x z.
Set l to be the term power_real_uniform_metric_value J x z.
Set u to be the term add_SNo (power_real_uniform_metric_value J x y) (power_real_uniform_metric_value J y z).
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 z HJne2 Hx Hz).
We prove the intermediate claim HlR: l ∈ R.
An exact proof term for the current goal is (R_lub_in_R A l Hlub).
We prove the intermediate claim HuR: u ∈ R.
An exact proof term for the current goal is (real_add_SNo (power_real_uniform_metric_value J x y) (power_real_uniform_metric_value_in_R J x y Hx Hy) (power_real_uniform_metric_value J y z) (power_real_uniform_metric_value_in_R J y z Hy Hz)).
We prove the intermediate claim Hub_u: ∀a : set, a ∈ A → a ∈ R → Rle a u.
Let a be given.
Assume HaA: a ∈ A.
Assume HaR: a ∈ R.
Apply (ReplE_impred J (λj : set ⇒ power_real_coord_clipped_diff x z j) a HaA (Rle a u)) to the current goal.
Let j be given.
Assume HjJ: j ∈ J.
Assume Haeq: a = power_real_coord_clipped_diff x z j.
rewrite the current goal using Haeq (from left to right).
Set axz to be the term power_real_coord_clipped_diff x z j.
Set axy to be the term power_real_coord_clipped_diff x y j.
Set ayz to be the term power_real_coord_clipped_diff y z j.
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 HzjR: apply_fun z j ∈ R.
An exact proof term for the current goal is (power_real_coord_in_R J z j HjJ Hz).
We prove the intermediate claim HaxzDef: axz = R_bounded_distance (apply_fun x j) (apply_fun z j).
An exact proof term for the current goal is (power_real_coord_clipped_diff_eq_R_bounded_distance J x z j HjJ Hx Hz).
We prove the intermediate claim HaxyDef: axy = 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 HayzDef: ayz = R_bounded_distance (apply_fun y j) (apply_fun z j).
An exact proof term for the current goal is (power_real_coord_clipped_diff_eq_R_bounded_distance J y z j HjJ Hy Hz).
We prove the intermediate claim HaxzR: axz ∈ R.
An exact proof term for the current goal is (power_real_clipped_diffs_in_R J x z axz Hx Hz (ReplI J (λk : set ⇒ power_real_coord_clipped_diff x z k) j HjJ)).
We prove the intermediate claim HaxyR: axy ∈ R.
An exact proof term for the current goal is (power_real_clipped_diffs_in_R J x y axy Hx Hy (ReplI J (λk : set ⇒ power_real_coord_clipped_diff x y k) j HjJ)).
We prove the intermediate claim HayzR: ayz ∈ R.
An exact proof term for the current goal is (power_real_clipped_diffs_in_R J y z ayz Hy Hz (ReplI J (λk : set ⇒ power_real_coord_clipped_diff y z k) j HjJ)).
We prove the intermediate claim HsumR: add_SNo axy ayz ∈ R.
An exact proof term for the current goal is (real_add_SNo axy HaxyR ayz HayzR).
We prove the intermediate claim HtriLeS: axz ≤ add_SNo axy ayz.
rewrite the current goal using HaxzDef (from left to right).
rewrite the current goal using HaxyDef (from left to right).
rewrite the current goal using HayzDef (from left to right).
An exact proof term for the current goal is (R_bounded_distance_triangle_Le (apply_fun x j) (apply_fun y j) (apply_fun z j) HxjR HyjR HzjR).
We prove the intermediate claim HtriLe: Rle axz (add_SNo axy ayz).
An exact proof term for the current goal is (Rle_of_SNoLe axz (add_SNo axy ayz) HaxzR HsumR HtriLeS).
We prove the intermediate claim Hlubxy: R_lub (power_real_clipped_diffs J x y) (power_real_uniform_metric_value J x y).
An exact proof term for the current goal is (power_real_uniform_metric_value_is_lub J x y HJne2 Hx Hy).
We prove the intermediate claim Hlubyz: R_lub (power_real_clipped_diffs J y z) (power_real_uniform_metric_value J y z).
An exact proof term for the current goal is (power_real_uniform_metric_value_is_lub J y z HJne2 Hy Hz).
We prove the intermediate claim Hxyub: ∀b : set, b ∈ power_real_clipped_diffs J x y → b ∈ R → Rle b (power_real_uniform_metric_value J x y).
An exact proof term for the current goal is (andER ((power_real_uniform_metric_value J x y) ∈ R) (∀b : set, b ∈ power_real_clipped_diffs J x y → b ∈ R → Rle b (power_real_uniform_metric_value J x y)) (andEL (((power_real_uniform_metric_value J x y) ∈ R) ∧ ∀b : set, b ∈ power_real_clipped_diffs J x y → b ∈ R → Rle b (power_real_uniform_metric_value J x y)) (∀uu : set, uu ∈ R → (∀b : set, b ∈ power_real_clipped_diffs J x y → b ∈ R → Rle b uu) → Rle (power_real_uniform_metric_value J x y) uu) Hlubxy)).
We prove the intermediate claim Hyzub: ∀b : set, b ∈ power_real_clipped_diffs J y z → b ∈ R → Rle b (power_real_uniform_metric_value J y z).
An exact proof term for the current goal is (andER ((power_real_uniform_metric_value J y z) ∈ R) (∀b : set, b ∈ power_real_clipped_diffs J y z → b ∈ R → Rle b (power_real_uniform_metric_value J y z)) (andEL (((power_real_uniform_metric_value J y z) ∈ R) ∧ ∀b : set, b ∈ power_real_clipped_diffs J y z → b ∈ R → Rle b (power_real_uniform_metric_value J y z)) (∀uu : set, uu ∈ R → (∀b : set, b ∈ power_real_clipped_diffs J y z → b ∈ R → Rle b uu) → Rle (power_real_uniform_metric_value J y z) uu) Hlubyz)).
We prove the intermediate claim Haxyub: Rle axy (power_real_uniform_metric_value J x y).
An exact proof term for the current goal is (Hxyub axy (ReplI J (λk : set ⇒ power_real_coord_clipped_diff x y k) j HjJ) HaxyR).
We prove the intermediate claim Hayzub: Rle ayz (power_real_uniform_metric_value J y z).
An exact proof term for the current goal is (Hyzub ayz (ReplI J (λk : set ⇒ power_real_coord_clipped_diff y z k) j HjJ) HayzR).
We prove the intermediate claim H2a: Rle (add_SNo axy ayz) (add_SNo axy (power_real_uniform_metric_value J y z)).
An exact proof term for the current goal is (Rle_add_SNo_2 axy ayz (power_real_uniform_metric_value J y z) HaxyR HayzR (power_real_uniform_metric_value_in_R J y z Hy Hz) Hayzub).
We prove the intermediate claim H2b: Rle (add_SNo axy (power_real_uniform_metric_value J y z)) u.
We prove the intermediate claim H2b': Rle (add_SNo (power_real_uniform_metric_value J y z) axy) (add_SNo (power_real_uniform_metric_value J y z) (power_real_uniform_metric_value J x y)).
An exact proof term for the current goal is (Rle_add_SNo_2 (power_real_uniform_metric_value J y z) axy (power_real_uniform_metric_value J x y) (power_real_uniform_metric_value_in_R J y z Hy Hz) HaxyR (power_real_uniform_metric_value_in_R J x y Hx Hy) Haxyub).
We prove the intermediate claim HcomL: add_SNo axy (power_real_uniform_metric_value J y z) = add_SNo (power_real_uniform_metric_value J y z) axy.
An exact proof term for the current goal is (add_SNo_com axy (power_real_uniform_metric_value J y z) (real_SNo axy HaxyR) (real_SNo (power_real_uniform_metric_value J y z) (power_real_uniform_metric_value_in_R J y z Hy Hz))).
We prove the intermediate claim HcomR: u = add_SNo (power_real_uniform_metric_value J y z) (power_real_uniform_metric_value J x y).
We prove the intermediate claim Hdefu: u = add_SNo (power_real_uniform_metric_value J x y) (power_real_uniform_metric_value J y z).
Use reflexivity.
rewrite the current goal using Hdefu (from left to right).
An exact proof term for the current goal is (add_SNo_com (power_real_uniform_metric_value J x y) (power_real_uniform_metric_value J y z) (real_SNo (power_real_uniform_metric_value J x y) (power_real_uniform_metric_value_in_R J x y Hx Hy)) (real_SNo (power_real_uniform_metric_value J y z) (power_real_uniform_metric_value_in_R J y z Hy Hz))).
rewrite the current goal using HcomL (from left to right).
rewrite the current goal using HcomR (from left to right).
An exact proof term for the current goal is H2b'.
We prove the intermediate claim H2: Rle (add_SNo axy ayz) u.
An exact proof term for the current goal is (Rle_tra (add_SNo axy ayz) (add_SNo axy (power_real_uniform_metric_value J y z)) u H2a H2b).
An exact proof term for the current goal is (Rle_tra axz (add_SNo axy ayz) u HtriLe H2).
We prove the intermediate claim Hmin: ∀uu : set, uu ∈ R → (∀a : set, a ∈ A → a ∈ R → Rle a uu) → Rle l uu.
An exact proof term for the current goal is (andER ((l ∈ R) ∧ ∀a : set, a ∈ A → a ∈ R → Rle a l) (∀uu : set, uu ∈ R → (∀a : set, a ∈ A → a ∈ R → Rle a uu) → Rle l uu) Hlub).
We prove the intermediate claim Hle: Rle l u.
An exact proof term for the current goal is (Hmin u HuR Hub_u).
An exact proof term for the current goal is (RleE_nlt l u Hle).
∎