Let X, d, x and y be given.
Assume Hm: metric_on X d.
Assume Hx: x ∈ X.
Assume Hy: y ∈ X.
Assume Hneq: ¬ (x = y).
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 HdR: apply_fun d (x,y) ∈ R.
An exact proof term for the current goal is (Hfun (x,y) HxyIn).
We prove the intermediate claim HdS: SNo (apply_fun d (x,y)).
An exact proof term for the current goal is (real_SNo (apply_fun d (x,y)) HdR).
Apply (SNoLt_trichotomy_or_impred (apply_fun d (x,y)) 0 HdS SNo_0 (Rlt 0 (apply_fun d (x,y)))) to the current goal.
Assume Hlt: apply_fun d (x,y) < 0.
We will prove Rlt 0 (apply_fun d (x,y)).
Apply FalseE to the current goal.
We prove the intermediate claim Hbad: Rlt (apply_fun d (x,y)) 0.
An exact proof term for the current goal is (RltI (apply_fun d (x,y)) 0 HdR real_0 Hlt).
An exact proof term for the current goal is ((metric_on_nonneg X d x y Hm Hx Hy) Hbad).
Assume Heq0: apply_fun d (x,y) = 0.
We will prove Rlt 0 (apply_fun d (x,y)).
Apply FalseE to the current goal.
We prove the intermediate claim Hxy: x = y.
An exact proof term for the current goal is (metric_on_zero_eq X d x y Hm Hx Hy Heq0).
An exact proof term for the current goal is (Hneq Hxy).
Assume H0lt: 0 < apply_fun d (x,y).
An exact proof term for the current goal is (RltI 0 (apply_fun d (x,y)) real_0 HdR H0lt).
∎