Let x, y and z be given.
Assume Hx: x ∈ R_omega_space.
Assume Hy: y ∈ R_omega_space.
Assume Hz: z ∈ R_omega_space.
Set A to be the term Romega_D_scaled_diffs x z.
Set l to be the term Romega_D_metric_value x z.
Set u to be the term add_SNo (Romega_D_metric_value x y) (Romega_D_metric_value y z).
We prove the intermediate claim Hlub: R_lub A l.
An exact proof term for the current goal is (Romega_D_metric_value_is_lub x z Hx Hz).
We prove the intermediate claim HuR: u ∈ R.
An exact proof term for the current goal is (real_add_SNo (Romega_D_metric_value x y) (Romega_D_metric_value_in_R x y Hx Hy) (Romega_D_metric_value y z) (Romega_D_metric_value_in_R y z Hy Hz)).
We prove the intermediate claim Hub: ∀a : set, a ∈ A → a ∈ R → Rle a u.
Let a be given.
Assume HaA: a ∈ A.
Assume HaR: a ∈ R.
Apply (ReplE_impred ω (λi : set ⇒ mul_SNo (R_bounded_distance (apply_fun x i) (apply_fun z i)) (inv_nat (ordsucc i))) a HaA (Rle a u)) to the current goal.
Let i be given.
Assume HiO: i ∈ ω.
Assume Hai: a = mul_SNo (R_bounded_distance (apply_fun x i) (apply_fun z i)) (inv_nat (ordsucc i)).
rewrite the current goal using Hai (from left to right).
Set inv to be the term inv_nat (ordsucc i).
Set bd_xz to be the term R_bounded_distance (apply_fun x i) (apply_fun z i).
Set bd_xy to be the term R_bounded_distance (apply_fun x i) (apply_fun y i).
Set bd_yz to be the term R_bounded_distance (apply_fun y i) (apply_fun z i).
Set sxz to be the term mul_SNo bd_xz inv.
Set sxy to be the term mul_SNo bd_xy inv.
Set syz to be the term mul_SNo bd_yz inv.
We prove the intermediate claim HxiR: apply_fun x i ∈ R.
An exact proof term for the current goal is (Romega_coord_in_R x i Hx HiO).
We prove the intermediate claim HyiR: apply_fun y i ∈ R.
An exact proof term for the current goal is (Romega_coord_in_R y i Hy HiO).
We prove the intermediate claim HziR: apply_fun z i ∈ R.
An exact proof term for the current goal is (Romega_coord_in_R z i Hz HiO).
We prove the intermediate claim HinvO: ordsucc i ∈ ω.
An exact proof term for the current goal is (omega_ordsucc i HiO).
We prove the intermediate claim HinvNot0: ordsucc i ∉ {0}.
Assume Hin0: ordsucc i ∈ {0}.
We prove the intermediate claim Heq: ordsucc i = 0.
An exact proof term for the current goal is (SingE 0 (ordsucc i) Hin0).
An exact proof term for the current goal is (neq_ordsucc_0 i Heq).
We prove the intermediate claim HinvIn: ordsucc i ∈ ω ∖ {0}.
An exact proof term for the current goal is (setminusI ω {0} (ordsucc i) HinvO HinvNot0).
We prove the intermediate claim HinvR: inv ∈ R.
An exact proof term for the current goal is (inv_nat_real (ordsucc i) HinvO).
We prove the intermediate claim HinvS: SNo inv.
An exact proof term for the current goal is (real_SNo inv HinvR).
We prove the intermediate claim HinvPosR: Rlt 0 inv.
An exact proof term for the current goal is (inv_nat_pos (ordsucc i) HinvIn).
We prove the intermediate claim HinvPos: 0 < inv.
An exact proof term for the current goal is (RltE_lt 0 inv HinvPosR).
We prove the intermediate claim HinvNN: 0 ≤ inv.
An exact proof term for the current goal is (SNoLtLe 0 inv HinvPos).
We prove the intermediate claim HbdxzR: bd_xz ∈ R.
An exact proof term for the current goal is (R_bounded_distance_in_R (apply_fun x i) (apply_fun z i) HxiR HziR).
We prove the intermediate claim HbdxyR: bd_xy ∈ R.
An exact proof term for the current goal is (R_bounded_distance_in_R (apply_fun x i) (apply_fun y i) HxiR HyiR).
We prove the intermediate claim HbdyzR: bd_yz ∈ R.
An exact proof term for the current goal is (R_bounded_distance_in_R (apply_fun y i) (apply_fun z i) HyiR HziR).
We prove the intermediate claim HbdxzS: SNo bd_xz.
An exact proof term for the current goal is (real_SNo bd_xz HbdxzR).
We prove the intermediate claim HbdxyS: SNo bd_xy.
An exact proof term for the current goal is (real_SNo bd_xy HbdxyR).
We prove the intermediate claim HbdyzS: SNo bd_yz.
An exact proof term for the current goal is (real_SNo bd_yz HbdyzR).
We prove the intermediate claim HbdTri: bd_xz ≤ add_SNo bd_xy bd_yz.
An exact proof term for the current goal is (R_bounded_distance_triangle_Le (apply_fun x i) (apply_fun y i) (apply_fun z i) HxiR HyiR HziR).
We prove the intermediate claim HmulLe: mul_SNo bd_xz inv ≤ mul_SNo (add_SNo bd_xy bd_yz) inv.
An exact proof term for the current goal is (nonneg_mul_SNo_Le' bd_xz (add_SNo bd_xy bd_yz) inv HbdxzS (SNo_add_SNo bd_xy bd_yz HbdxyS HbdyzS) HinvS HinvNN HbdTri).
We prove the intermediate claim HmulEq: mul_SNo (add_SNo bd_xy bd_yz) inv = add_SNo (mul_SNo bd_xy inv) (mul_SNo bd_yz inv).
An exact proof term for the current goal is (mul_SNo_distrR bd_xy bd_yz inv HbdxyS HbdyzS HinvS).
We prove the intermediate claim HsxzLe: sxz ≤ add_SNo sxy syz.
rewrite the current goal using HmulEq (from right to left).
An exact proof term for the current goal is HmulLe.
We prove the intermediate claim HsxzR: sxz ∈ R.
An exact proof term for the current goal is (real_mul_SNo bd_xz HbdxzR inv HinvR).
We prove the intermediate claim HsumR: add_SNo sxy syz ∈ R.
An exact proof term for the current goal is (real_add_SNo sxy (real_mul_SNo bd_xy HbdxyR inv HinvR) syz (real_mul_SNo bd_yz HbdyzR inv HinvR)).
We prove the intermediate claim H1: Rle sxz (add_SNo sxy syz).
An exact proof term for the current goal is (Rle_of_SNoLe sxz (add_SNo sxy syz) HsxzR HsumR HsxzLe).
We prove the intermediate claim Hlubxy: R_lub (Romega_D_scaled_diffs x y) (Romega_D_metric_value x y).
An exact proof term for the current goal is (Romega_D_metric_value_is_lub x y Hx Hy).
We prove the intermediate claim Hlubyz: R_lub (Romega_D_scaled_diffs y z) (Romega_D_metric_value y z).
An exact proof term for the current goal is (Romega_D_metric_value_is_lub y z Hy Hz).
We prove the intermediate claim Hxyub: ∀b : set, b ∈ Romega_D_scaled_diffs x y → b ∈ R → Rle b (Romega_D_metric_value x y).
An exact proof term for the current goal is (andER ((Romega_D_metric_value x y) ∈ R) (∀b : set, b ∈ Romega_D_scaled_diffs x y → b ∈ R → Rle b (Romega_D_metric_value x y)) (andEL (((Romega_D_metric_value x y) ∈ R) ∧ ∀b : set, b ∈ Romega_D_scaled_diffs x y → b ∈ R → Rle b (Romega_D_metric_value x y)) (∀uu : set, uu ∈ R → (∀b : set, b ∈ Romega_D_scaled_diffs x y → b ∈ R → Rle b uu) → Rle (Romega_D_metric_value x y) uu) Hlubxy)).
We prove the intermediate claim Hyzub: ∀b : set, b ∈ Romega_D_scaled_diffs y z → b ∈ R → Rle b (Romega_D_metric_value y z).
An exact proof term for the current goal is (andER ((Romega_D_metric_value y z) ∈ R) (∀b : set, b ∈ Romega_D_scaled_diffs y z → b ∈ R → Rle b (Romega_D_metric_value y z)) (andEL (((Romega_D_metric_value y z) ∈ R) ∧ ∀b : set, b ∈ Romega_D_scaled_diffs y z → b ∈ R → Rle b (Romega_D_metric_value y z)) (∀uu : set, uu ∈ R → (∀b : set, b ∈ Romega_D_scaled_diffs y z → b ∈ R → Rle b uu) → Rle (Romega_D_metric_value y z) uu) Hlubyz)).
We prove the intermediate claim HsxyA: sxy ∈ Romega_D_scaled_diffs x y.
An exact proof term for the current goal is (ReplI ω (λj : set ⇒ mul_SNo (R_bounded_distance (apply_fun x j) (apply_fun y j)) (inv_nat (ordsucc j))) i HiO).
We prove the intermediate claim HsyzA: syz ∈ Romega_D_scaled_diffs y z.
An exact proof term for the current goal is (ReplI ω (λj : set ⇒ mul_SNo (R_bounded_distance (apply_fun y j) (apply_fun z j)) (inv_nat (ordsucc j))) i HiO).
We prove the intermediate claim HsxyR: sxy ∈ R.
An exact proof term for the current goal is (real_mul_SNo bd_xy HbdxyR inv HinvR).
We prove the intermediate claim HsyzR: syz ∈ R.
An exact proof term for the current goal is (real_mul_SNo bd_yz HbdyzR inv HinvR).
We prove the intermediate claim Hsxyub: Rle sxy (Romega_D_metric_value x y).
An exact proof term for the current goal is (Hxyub sxy HsxyA HsxyR).
We prove the intermediate claim Hsyzub: Rle syz (Romega_D_metric_value y z).
An exact proof term for the current goal is (Hyzub syz HsyzA HsyzR).
We prove the intermediate claim H2a: Rle (add_SNo sxy syz) (add_SNo sxy (Romega_D_metric_value y z)).
An exact proof term for the current goal is (Rle_add_SNo_2 sxy syz (Romega_D_metric_value y z) HsxyR HsyzR (Romega_D_metric_value_in_R y z Hy Hz) Hsyzub).
We prove the intermediate claim H2b': Rle (add_SNo (Romega_D_metric_value y z) sxy) (add_SNo (Romega_D_metric_value y z) (Romega_D_metric_value x y)).
An exact proof term for the current goal is (Rle_add_SNo_2 (Romega_D_metric_value y z) sxy (Romega_D_metric_value x y) (Romega_D_metric_value_in_R y z Hy Hz) HsxyR (Romega_D_metric_value_in_R x y Hx Hy) Hsxyub).
We prove the intermediate claim H2b: Rle (add_SNo sxy (Romega_D_metric_value y z)) u.
We prove the intermediate claim HcomL: add_SNo sxy (Romega_D_metric_value y z) = add_SNo (Romega_D_metric_value y z) sxy.
An exact proof term for the current goal is (add_SNo_com sxy (Romega_D_metric_value y z) (real_SNo sxy HsxyR) (real_SNo (Romega_D_metric_value y z) (Romega_D_metric_value_in_R y z Hy Hz))).
We prove the intermediate claim HcomR: u = add_SNo (Romega_D_metric_value y z) (Romega_D_metric_value x y).
An exact proof term for the current goal is (add_SNo_com (Romega_D_metric_value x y) (Romega_D_metric_value y z) (real_SNo (Romega_D_metric_value x y) (Romega_D_metric_value_in_R x y Hx Hy)) (real_SNo (Romega_D_metric_value y z) (Romega_D_metric_value_in_R 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 sxy syz) u.
An exact proof term for the current goal is (Rle_tra (add_SNo sxy syz) (add_SNo sxy (Romega_D_metric_value y z)) u H2a H2b).
An exact proof term for the current goal is (Rle_tra sxz (add_SNo sxy syz) u H1 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).
An exact proof term for the current goal is (RleE_nlt l u Hle).
∎