Let X, d, x and r be given.

Assume Hm: metric_on X d.

Assume Hx: x ∈ X.

Assume Hr: Rlt 0 r.

We prove the intermediate claim Hdxx0: apply_fun d (x,x) = 0.

An exact proof term for the current goal is (metric_on_diag_zero X d x Hm Hx).

We prove the intermediate claim Hpred: Rlt (apply_fun d (x,x)) r.

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

An exact proof term for the current goal is Hr.

An exact proof term for the current goal is (SepI X (λy0 : set ⇒ Rlt (apply_fun d (x,y0)) r) x Hx Hpred).

∎