Let c and r be given.
Assume HcR: c ∈ R.
Assume HrR: r ∈ R.
Assume Hrpos: Rlt 0 r.
We prove the intermediate claim HcS: SNo c.
An exact proof term for the current goal is (real_SNo c HcR).
We prove the intermediate claim HrS: SNo r.
An exact proof term for the current goal is (real_SNo r HrR).
We prove the intermediate claim HrposS: 0 < r.
An exact proof term for the current goal is (RltE_lt 0 r Hrpos).
Apply (SNoLt_trichotomy_or_impred r 1 HrS SNo_1 (open_ball R R_bounded_metric c r ∈ R_standard_topology)) to the current goal.
Assume Hrlt1S: r < 1.
We prove the intermediate claim Hrlt1: Rlt r 1.
An exact proof term for the current goal is (RltI r 1 HrR real_1 Hrlt1S).
We prove the intermediate claim HmrcR: minus_SNo r ∈ R.
An exact proof term for the current goal is (real_minus_SNo r HrR).
We prove the intermediate claim HmrcS: SNo (minus_SNo r).
An exact proof term for the current goal is (real_SNo (minus_SNo r) HmrcR).
We prove the intermediate claim Hneglt0: minus_SNo r < 0.
rewrite the current goal using minus_SNo_0 (from right to left).
An exact proof term for the current goal is (minus_SNo_Lt_contra 0 r SNo_0 HrS HrposS).
We prove the intermediate claim Hneglt: minus_SNo r < r.
An exact proof term for the current goal is (SNoLt_tra (minus_SNo r) 0 r HmrcS SNo_0 HrS Hneglt0 HrposS).
We prove the intermediate claim HcprR: add_SNo c r ∈ R.
An exact proof term for the current goal is (real_add_SNo c HcR r HrR).
We prove the intermediate claim HcmrR: add_SNo c (minus_SNo r) ∈ R.
An exact proof term for the current goal is (real_add_SNo c HcR (minus_SNo r) HmrcR).
We prove the intermediate claim HcmrS: SNo (add_SNo c (minus_SNo r)).
An exact proof term for the current goal is (real_SNo (add_SNo c (minus_SNo r)) HcmrR).
We prove the intermediate claim HcprS: SNo (add_SNo c r).
An exact proof term for the current goal is (real_SNo (add_SNo c r) HcprR).
We prove the intermediate claim HltS: add_SNo c (minus_SNo r) < add_SNo c r.
An exact proof term for the current goal is (add_SNo_Lt2 c (minus_SNo r) r HcS HmrcS HrS Hneglt).
We prove the intermediate claim Hlt: Rlt (add_SNo c (minus_SNo r)) (add_SNo c r).
An exact proof term for the current goal is (RltI (add_SNo c (minus_SNo r)) (add_SNo c r) HcmrR HcprR HltS).
rewrite the current goal using (open_ball_R_bounded_metric_eq_open_interval_early c r HcR HrR Hrpos Hrlt1) (from left to right).
An exact proof term for the current goal is (open_interval_in_R_standard_topology (add_SNo c (minus_SNo r)) (add_SNo c r) Hlt).
Assume HrEq: r = 1.
rewrite the current goal using HrEq (from left to right).
rewrite the current goal using (open_ball_R_bounded_metric_r1_eq_open_interval_early c HcR) (from left to right).
We prove the intermediate claim Hm1R: minus_SNo 1 ∈ R.
An exact proof term for the current goal is (real_minus_SNo 1 real_1).
We prove the intermediate claim Hm1S: SNo (minus_SNo 1).
An exact proof term for the current goal is (real_SNo (minus_SNo 1) Hm1R).
We prove the intermediate claim Hm1lt0: minus_SNo 1 < 0.
An exact proof term for the current goal is minus_1_lt_0.
We prove the intermediate claim Hm1lt1: minus_SNo 1 < 1.
An exact proof term for the current goal is (SNoLt_tra (minus_SNo 1) 0 1 Hm1S SNo_0 SNo_1 Hm1lt0 SNoLt_0_1).
We prove the intermediate claim HcprR: add_SNo c 1 ∈ R.
An exact proof term for the current goal is (real_add_SNo c HcR 1 real_1).
We prove the intermediate claim HcmrR: add_SNo c (minus_SNo 1) ∈ R.
An exact proof term for the current goal is (real_add_SNo c HcR (minus_SNo 1) Hm1R).
We prove the intermediate claim HcmrS: SNo (add_SNo c (minus_SNo 1)).
An exact proof term for the current goal is (real_SNo (add_SNo c (minus_SNo 1)) HcmrR).
We prove the intermediate claim HcprS: SNo (add_SNo c 1).
An exact proof term for the current goal is (real_SNo (add_SNo c 1) HcprR).
We prove the intermediate claim HltS: add_SNo c (minus_SNo 1) < add_SNo c 1.
An exact proof term for the current goal is (add_SNo_Lt2 c (minus_SNo 1) 1 HcS Hm1S SNo_1 Hm1lt1).
We prove the intermediate claim Hlt: Rlt (add_SNo c (minus_SNo 1)) (add_SNo c 1).
An exact proof term for the current goal is (RltI (add_SNo c (minus_SNo 1)) (add_SNo c 1) HcmrR HcprR HltS).
An exact proof term for the current goal is (open_interval_in_R_standard_topology (add_SNo c (minus_SNo 1)) (add_SNo c 1) Hlt).
Assume H1ltrS: 1 < r.
We prove the intermediate claim H1ltr: Rlt 1 r.
An exact proof term for the current goal is (RltI 1 r real_1 HrR H1ltrS).
rewrite the current goal using (open_ball_R_bounded_metric_eq_R_if_1_lt_early c r HcR HrR H1ltr) (from left to right).
An exact proof term for the current goal is (topology_has_X R R_standard_topology (R_standard_topology_is_topology_local)).
∎