Let X, d, x, r1 and r2 be given.

Assume Hr: Rlt r1 r2.

Let y be given.

Assume Hy: y ∈ open_ball X d x r1.

We will prove y ∈ open_ball X d x r2.

We prove the intermediate claim HyX: y ∈ X.

An exact proof term for the current goal is (open_ballE1 X d x r1 y Hy).

We prove the intermediate claim Hdlt: Rlt (apply_fun d (x,y)) r1.

An exact proof term for the current goal is (open_ballE2 X d x r1 y Hy).

We prove the intermediate claim Hdlt2: Rlt (apply_fun d (x,y)) r2.

An exact proof term for the current goal is (Rlt_tra (apply_fun d (x,y)) r1 r2 Hdlt Hr).

An exact proof term for the current goal is (open_ballI X d x r2 y HyX Hdlt2).

∎