Let a be given.

Assume HaA: a ∈ A.

Assume HaR: a ∈ R.

Apply (ReplE_impred ω (λn : set ⇒ Romega_coord_clipped_diff x z n) a HaA (Rle a u)) to the current goal.

Let n be given.

Assume HnO: n ∈ ω.

Assume Haeq: a = Romega_coord_clipped_diff x z n.

rewrite the current goal using Haeq (from left to right).

Set axz to be the term Romega_coord_clipped_diff x z n.

Set axy to be the term Romega_coord_clipped_diff x y n.

Set ayz to be the term Romega_coord_clipped_diff y z n.

We prove the intermediate claim HaxzLe: axz ≤ add_SNo axy ayz.

An exact proof term for the current goal is (Romega_coord_clipped_diff_triangle x y z n Hx Hy Hz HnO).

We prove the intermediate claim HaxzR: axz ∈ R.

An exact proof term for the current goal is (Romega_clipped_diffs_in_R x z Hx Hz axz (ReplI ω (λk : set ⇒ Romega_coord_clipped_diff x z k) n HnO)).

We prove the intermediate claim HaxyR: axy ∈ R.

An exact proof term for the current goal is (Romega_clipped_diffs_in_R x y Hx Hy axy (ReplI ω (λk : set ⇒ Romega_coord_clipped_diff x y k) n HnO)).

We prove the intermediate claim HayzR: ayz ∈ R.

An exact proof term for the current goal is (Romega_clipped_diffs_in_R y z Hy Hz ayz (ReplI ω (λk : set ⇒ Romega_coord_clipped_diff y z k) n HnO)).

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 H1: 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 HaxzLe).

We prove the intermediate claim Hlubxy: R_lub (Romega_clipped_diffs x y) (Romega_uniform_metric_value x y).

An exact proof term for the current goal is (Romega_uniform_metric_value_is_lub x y Hx Hy).

We prove the intermediate claim Hlubyz: R_lub (Romega_clipped_diffs y z) (Romega_uniform_metric_value y z).

An exact proof term for the current goal is (Romega_uniform_metric_value_is_lub y z Hy Hz).

We prove the intermediate claim Hxyub: ∀b : set, b ∈ Romega_clipped_diffs x y → b ∈ R → Rle b (Romega_uniform_metric_value x y).

An exact proof term for the current goal is (andER ((Romega_uniform_metric_value x y) ∈ R) (∀b : set, b ∈ Romega_clipped_diffs x y → b ∈ R → Rle b (Romega_uniform_metric_value x y)) (andEL (((Romega_uniform_metric_value x y) ∈ R) ∧ ∀b : set, b ∈ Romega_clipped_diffs x y → b ∈ R → Rle b (Romega_uniform_metric_value x y)) (∀uu : set, uu ∈ R → (∀b : set, b ∈ Romega_clipped_diffs x y → b ∈ R → Rle b uu) → Rle (Romega_uniform_metric_value x y) uu) Hlubxy)).

We prove the intermediate claim Hyzub: ∀b : set, b ∈ Romega_clipped_diffs y z → b ∈ R → Rle b (Romega_uniform_metric_value y z).

An exact proof term for the current goal is (andER ((Romega_uniform_metric_value y z) ∈ R) (∀b : set, b ∈ Romega_clipped_diffs y z → b ∈ R → Rle b (Romega_uniform_metric_value y z)) (andEL (((Romega_uniform_metric_value y z) ∈ R) ∧ ∀b : set, b ∈ Romega_clipped_diffs y z → b ∈ R → Rle b (Romega_uniform_metric_value y z)) (∀uu : set, uu ∈ R → (∀b : set, b ∈ Romega_clipped_diffs y z → b ∈ R → Rle b uu) → Rle (Romega_uniform_metric_value y z) uu) Hlubyz)).

We prove the intermediate claim Haxyub: Rle axy (Romega_uniform_metric_value x y).

An exact proof term for the current goal is (Hxyub axy (ReplI ω (λk : set ⇒ Romega_coord_clipped_diff x y k) n HnO) HaxyR).

We prove the intermediate claim Hayzub: Rle ayz (Romega_uniform_metric_value y z).

An exact proof term for the current goal is (Hyzub ayz (ReplI ω (λk : set ⇒ Romega_coord_clipped_diff y z k) n HnO) HayzR).

We prove the intermediate claim H2a: Rle (add_SNo axy ayz) (add_SNo axy (Romega_uniform_metric_value y z)).

An exact proof term for the current goal is (Rle_add_SNo_2 axy ayz (Romega_uniform_metric_value y z) HaxyR HayzR (Romega_uniform_metric_value_in_R y z Hy Hz) Hayzub).

We prove the intermediate claim H2b': Rle (add_SNo (Romega_uniform_metric_value y z) axy) (add_SNo (Romega_uniform_metric_value y z) (Romega_uniform_metric_value x y)).

An exact proof term for the current goal is (Rle_add_SNo_2 (Romega_uniform_metric_value y z) axy (Romega_uniform_metric_value x y) (Romega_uniform_metric_value_in_R y z Hy Hz) HaxyR (Romega_uniform_metric_value_in_R x y Hx Hy) Haxyub).

We prove the intermediate claim H2b: Rle (add_SNo axy (Romega_uniform_metric_value y z)) (add_SNo (Romega_uniform_metric_value x y) (Romega_uniform_metric_value y z)).

We prove the intermediate claim HcomL: add_SNo axy (Romega_uniform_metric_value y z) = add_SNo (Romega_uniform_metric_value y z) axy.

An exact proof term for the current goal is (add_SNo_com axy (Romega_uniform_metric_value y z) (real_SNo axy HaxyR) (real_SNo (Romega_uniform_metric_value y z) (Romega_uniform_metric_value_in_R y z Hy Hz))).

We prove the intermediate claim HcomR: add_SNo (Romega_uniform_metric_value x y) (Romega_uniform_metric_value y z) = add_SNo (Romega_uniform_metric_value y z) (Romega_uniform_metric_value x y).

An exact proof term for the current goal is (add_SNo_com (Romega_uniform_metric_value x y) (Romega_uniform_metric_value y z) (real_SNo (Romega_uniform_metric_value x y) (Romega_uniform_metric_value_in_R x y Hx Hy)) (real_SNo (Romega_uniform_metric_value y z) (Romega_uniform_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 axy ayz) u.

An exact proof term for the current goal is (Rle_tra (add_SNo axy ayz) (add_SNo axy (Romega_uniform_metric_value y z)) u H2a H2b).

An exact proof term for the current goal is (Rle_tra axz (add_SNo axy ayz) u H1 H2).