Let X, d, x, y and z be given.
Assume Hm: metric_on X d.
Assume Hx: x ∈ X.
Assume Hy: y ∈ X.
Assume Hz: z ∈ X.
We prove the intermediate claim Hfun: function_on d (setprod X X) R.
An exact proof term for the current goal is (metric_on_function_on X d Hm).
We prove the intermediate claim HxyIn: (x,y) ∈ setprod X X.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma X X x y Hx Hy).
We prove the intermediate claim HyzIn: (y,z) ∈ setprod X X.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma X X y z Hy Hz).
We prove the intermediate claim HxzIn: (x,z) ∈ setprod X X.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma X X x z Hx Hz).
We prove the intermediate claim HdxyR: apply_fun d (x,y) ∈ R.
An exact proof term for the current goal is (Hfun (x,y) HxyIn).
We prove the intermediate claim HdyzR: apply_fun d (y,z) ∈ R.
An exact proof term for the current goal is (Hfun (y,z) HyzIn).
We prove the intermediate claim HdxzR: apply_fun d (x,z) ∈ R.
An exact proof term for the current goal is (Hfun (x,z) HxzIn).
We prove the intermediate claim HsumR: add_SNo (apply_fun d (x,y)) (apply_fun d (y,z)) ∈ R.
An exact proof term for the current goal is (real_add_SNo (apply_fun d (x,y)) HdxyR (apply_fun d (y,z)) HdyzR).
An exact proof term for the current goal is (RleI (apply_fun d (x,z)) (add_SNo (apply_fun d (x,y)) (apply_fun d (y,z))) HdxzR HsumR (metric_on_triangle X d x y z Hm Hx Hy Hz)).
∎