Let c and r be given.
Assume HcR: c ∈ R.
Assume HrR: r ∈ R.
Assume HrposR: Rlt 0 r.
Assume Hrlt1R: Rlt r 1.
Apply set_ext to the current goal.
Let y be given.
Assume HyB: y ∈ open_ball R R_bounded_metric c r.
We will prove y ∈ open_interval (add_SNo c (minus_SNo r)) (add_SNo c r).
We prove the intermediate claim HdefI: open_interval (add_SNo c (minus_SNo r)) (add_SNo c r) = {x ∈ R|Rlt (add_SNo c (minus_SNo r)) x ∧ Rlt x (add_SNo c r)}.
Use reflexivity.
rewrite the current goal using HdefI (from left to right).
We prove the intermediate claim HyR: y ∈ R.
An exact proof term for the current goal is (open_ballE1 R R_bounded_metric c r y HyB).
We prove the intermediate claim Hdlt: Rlt (apply_fun R_bounded_metric (c,y)) r.
An exact proof term for the current goal is (open_ballE2 R R_bounded_metric c r y HyB).
We prove the intermediate claim Hbdlt: Rlt (R_bounded_distance c y) r.
rewrite the current goal using (R_bounded_metric_apply c y HcR HyR) (from right to left).
An exact proof term for the current goal is Hdlt.
We prove the intermediate claim Habslt: abs_SNo (add_SNo c (minus_SNo y)) < r.
An exact proof term for the current goal is (R_bounded_distance_lt_lt1_imp_abs_lt c y r HcR HyR HrR Hrlt1R Hbdlt).
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 HyS: SNo y.
An exact proof term for the current goal is (real_SNo y HyR).
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 HrposR).
Set t to be the term add_SNo c (minus_SNo y).
We prove the intermediate claim HmyS: SNo (minus_SNo y).
An exact proof term for the current goal is (SNo_minus_SNo y HyS).
We prove the intermediate claim HtS: SNo t.
An exact proof term for the current goal is (SNo_add_SNo c (minus_SNo y) HcS HmyS).
We prove the intermediate claim Htlt: t < r.
An exact proof term for the current goal is (abs_SNo_lt_imp_lt t r HtS HrS HrposS Habslt).
We prove the intermediate claim Hmtlt: minus_SNo t < r.
An exact proof term for the current goal is (abs_SNo_lt_imp_neg_lt t r HtS HrS HrposS Habslt).
We prove the intermediate claim Hswap: add_SNo y (minus_SNo c) = minus_SNo (add_SNo c (minus_SNo y)).
We prove the intermediate claim HmcS: SNo (minus_SNo c).
An exact proof term for the current goal is (SNo_minus_SNo c HcS).
We prove the intermediate claim Hneg: minus_SNo (add_SNo c (minus_SNo y)) = add_SNo (minus_SNo c) (minus_SNo (minus_SNo y)).
An exact proof term for the current goal is (minus_add_SNo_distr c (minus_SNo y) HcS HmyS).
We prove the intermediate claim Hinv: minus_SNo (minus_SNo y) = y.
An exact proof term for the current goal is (minus_SNo_invol y HyS).
We prove the intermediate claim Hneg2: minus_SNo (add_SNo c (minus_SNo y)) = add_SNo (minus_SNo c) y.
rewrite the current goal using Hinv (from right to left) at position 2.
An exact proof term for the current goal is Hneg.
We prove the intermediate claim Hcom: add_SNo (minus_SNo c) y = add_SNo y (minus_SNo c).
An exact proof term for the current goal is (add_SNo_com (minus_SNo c) y HmcS HyS).
We will prove add_SNo y (minus_SNo c) = minus_SNo (add_SNo c (minus_SNo y)).
rewrite the current goal using Hcom (from right to left).
rewrite the current goal using Hneg2 (from right to left).
Use reflexivity.
We prove the intermediate claim HycLt: add_SNo y (minus_SNo c) < r.
rewrite the current goal using Hswap (from left to right).
An exact proof term for the current goal is Hmtlt.
We prove the intermediate claim HyLt: y < add_SNo c r.
We prove the intermediate claim Hlt1: y < add_SNo r c.
An exact proof term for the current goal is (add_SNo_minus_Lt1 y c r HyS HcS HrS HycLt).
We prove the intermediate claim Hcom: add_SNo r c = add_SNo c r.
An exact proof term for the current goal is (add_SNo_com r c HrS HcS).
rewrite the current goal using Hcom (from right to left).
An exact proof term for the current goal is Hlt1.
We prove the intermediate claim HcmyLt: add_SNo c (minus_SNo r) < y.
We prove the intermediate claim Hlt1: c < add_SNo r y.
An exact proof term for the current goal is (add_SNo_minus_Lt1 c y r HcS HyS HrS Htlt).
We prove the intermediate claim Hcom1: add_SNo r y = add_SNo y r.
An exact proof term for the current goal is (add_SNo_com r y HrS HyS).
We prove the intermediate claim Hlt2: c < add_SNo y r.
rewrite the current goal using Hcom1 (from right to left).
An exact proof term for the current goal is Hlt1.
We prove the intermediate claim HmrS: SNo (minus_SNo r).
An exact proof term for the current goal is (SNo_minus_SNo r HrS).
We prove the intermediate claim HyrS: SNo (add_SNo y r).
An exact proof term for the current goal is (SNo_add_SNo y r HyS HrS).
An exact proof term for the current goal is (add_SNo_minus_Lt1b c r y HcS HrS HyS Hlt2).
We prove the intermediate claim HcrR: add_SNo c (minus_SNo r) ∈ R.
An exact proof term for the current goal is (real_add_SNo c HcR (minus_SNo r) (real_minus_SNo r HrR)).
We prove the intermediate claim HcrS: SNo (add_SNo c (minus_SNo r)).
An exact proof term for the current goal is (real_SNo (add_SNo c (minus_SNo r)) HcrR).
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 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 HleftRlt: Rlt (add_SNo c (minus_SNo r)) y.
An exact proof term for the current goal is (RltI (add_SNo c (minus_SNo r)) y HcrR HyR HcmyLt).
We prove the intermediate claim HrightRlt: Rlt y (add_SNo c r).
An exact proof term for the current goal is (RltI y (add_SNo c r) HyR HcprR HyLt).
An exact proof term for the current goal is (SepI R (λx0 : set ⇒ Rlt (add_SNo c (minus_SNo r)) x0 ∧ Rlt x0 (add_SNo c r)) y HyR (andI (Rlt (add_SNo c (minus_SNo r)) y) (Rlt y (add_SNo c r)) HleftRlt HrightRlt)).
Let y be given.
Assume HyI: y ∈ open_interval (add_SNo c (minus_SNo r)) (add_SNo c r).
We will prove y ∈ open_ball R R_bounded_metric c r.
We prove the intermediate claim HdefI: open_interval (add_SNo c (minus_SNo r)) (add_SNo c r) = {x ∈ R|Rlt (add_SNo c (minus_SNo r)) x ∧ Rlt x (add_SNo c r)}.
Use reflexivity.
We prove the intermediate claim HyI': y ∈ {x ∈ R|Rlt (add_SNo c (minus_SNo r)) x ∧ Rlt x (add_SNo c r)}.
rewrite the current goal using HdefI (from right to left).
An exact proof term for the current goal is HyI.
We prove the intermediate claim HyR: y ∈ R.
An exact proof term for the current goal is (SepE1 R (λx0 : set ⇒ Rlt (add_SNo c (minus_SNo r)) x0 ∧ Rlt x0 (add_SNo c r)) y HyI').
We prove the intermediate claim Hconj: Rlt (add_SNo c (minus_SNo r)) y ∧ Rlt y (add_SNo c r).
An exact proof term for the current goal is (SepE2 R (λx0 : set ⇒ Rlt (add_SNo c (minus_SNo r)) x0 ∧ Rlt x0 (add_SNo c r)) y HyI').
We prove the intermediate claim Hleft: Rlt (add_SNo c (minus_SNo r)) y.
An exact proof term for the current goal is (andEL (Rlt (add_SNo c (minus_SNo r)) y) (Rlt y (add_SNo c r)) Hconj).
We prove the intermediate claim Hright: Rlt y (add_SNo c r).
An exact proof term for the current goal is (andER (Rlt (add_SNo c (minus_SNo r)) y) (Rlt y (add_SNo c r)) Hconj).
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 HyS: SNo y.
An exact proof term for the current goal is (real_SNo y HyR).
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 H0lt: 0 < r.
An exact proof term for the current goal is (RltE_lt 0 r HrposR).
We prove the intermediate claim HltY: y < add_SNo c r.
An exact proof term for the current goal is (RltE_lt y (add_SNo c r) Hright).
We prove the intermediate claim Hcylt: add_SNo c (minus_SNo r) < y.
An exact proof term for the current goal is (RltE_lt (add_SNo c (minus_SNo r)) y Hleft).
We prove the intermediate claim HycLt: add_SNo y (minus_SNo c) < r.
We prove the intermediate claim HcprS: SNo (add_SNo c r).
An exact proof term for the current goal is (SNo_add_SNo c r HcS HrS).
We prove the intermediate claim Hcom: add_SNo c r = add_SNo r c.
An exact proof term for the current goal is (add_SNo_com c r HcS HrS).
We prove the intermediate claim Hlt2: y < add_SNo r c.
rewrite the current goal using Hcom (from right to left).
An exact proof term for the current goal is HltY.
An exact proof term for the current goal is (add_SNo_minus_Lt1b y c r HyS HcS HrS Hlt2).
We prove the intermediate claim HcyLt: add_SNo c (minus_SNo y) < r.
We prove the intermediate claim HmrS: SNo (minus_SNo r).
An exact proof term for the current goal is (SNo_minus_SNo r HrS).
We prove the intermediate claim HmR: minus_SNo r ∈ R.
An exact proof term for the current goal is (real_minus_SNo r HrR).
We prove the intermediate claim HmS: SNo (minus_SNo r).
An exact proof term for the current goal is (real_SNo (minus_SNo r) HmR).
We prove the intermediate claim Hsum: add_SNo r (add_SNo c (minus_SNo r)) < add_SNo r y.
An exact proof term for the current goal is (add_SNo_Lt2 r (add_SNo c (minus_SNo r)) y HrS (SNo_add_SNo c (minus_SNo r) HcS (SNo_minus_SNo r HrS)) HyS Hcylt).
We prove the intermediate claim Hassoc1: add_SNo r (add_SNo c (minus_SNo r)) = add_SNo (add_SNo r c) (minus_SNo r).
An exact proof term for the current goal is (add_SNo_assoc r c (minus_SNo r) HrS HcS (SNo_minus_SNo r HrS)).
We prove the intermediate claim Hcom2: add_SNo r c = add_SNo c r.
An exact proof term for the current goal is (add_SNo_com r c HrS HcS).
We prove the intermediate claim Hassoc2: add_SNo (add_SNo r c) (minus_SNo r) = add_SNo c (add_SNo r (minus_SNo r)).
rewrite the current goal using Hcom2 (from left to right).
rewrite the current goal using (add_SNo_assoc c r (minus_SNo r) HcS HrS (SNo_minus_SNo r HrS)) (from right to left).
Use reflexivity.
We prove the intermediate claim Hrinv: add_SNo r (minus_SNo r) = 0.
An exact proof term for the current goal is (add_SNo_minus_SNo_rinv r HrS).
We prove the intermediate claim Heqleft: add_SNo r (add_SNo c (minus_SNo r)) = c.
rewrite the current goal using Hassoc1 (from left to right).
rewrite the current goal using Hassoc2 (from left to right).
rewrite the current goal using Hrinv (from left to right).
rewrite the current goal using (add_SNo_0R c HcS) (from left to right).
Use reflexivity.
We prove the intermediate claim Hlt3: c < add_SNo r y.
rewrite the current goal using Heqleft (from right to left).
An exact proof term for the current goal is Hsum.
An exact proof term for the current goal is (add_SNo_minus_Lt1b c y r HcS HyS HrS Hlt3).
Set t to be the term add_SNo c (minus_SNo y).
We prove the intermediate claim HmyS: SNo (minus_SNo y).
An exact proof term for the current goal is (SNo_minus_SNo y HyS).
We prove the intermediate claim HtS: SNo t.
An exact proof term for the current goal is (SNo_add_SNo c (minus_SNo y) HcS HmyS).
We prove the intermediate claim Hablt: abs_SNo t < r.
Apply (xm (0 ≤ t)) to the current goal.
Assume H0le: 0 ≤ t.
rewrite the current goal using (nonneg_abs_SNo t H0le) (from left to right).
An exact proof term for the current goal is HcyLt.
Assume Hn0le: ¬ (0 ≤ t).
rewrite the current goal using (not_nonneg_abs_SNo t Hn0le) (from left to right).
We prove the intermediate claim Hswap: minus_SNo t = add_SNo y (minus_SNo c).
We prove the intermediate claim HmcS: SNo (minus_SNo c).
An exact proof term for the current goal is (SNo_minus_SNo c HcS).
We prove the intermediate claim Hneg: minus_SNo (add_SNo c (minus_SNo y)) = add_SNo (minus_SNo c) (minus_SNo (minus_SNo y)).
An exact proof term for the current goal is (minus_add_SNo_distr c (minus_SNo y) HcS HmyS).
We prove the intermediate claim Hinv: minus_SNo (minus_SNo y) = y.
An exact proof term for the current goal is (minus_SNo_invol y HyS).
We prove the intermediate claim Hneg2: minus_SNo (add_SNo c (minus_SNo y)) = add_SNo (minus_SNo c) y.
rewrite the current goal using Hinv (from right to left) at position 2.
An exact proof term for the current goal is Hneg.
We prove the intermediate claim Hcom: add_SNo (minus_SNo c) y = add_SNo y (minus_SNo c).
An exact proof term for the current goal is (add_SNo_com (minus_SNo c) y HmcS HyS).
We will prove minus_SNo t = add_SNo y (minus_SNo c).
We prove the intermediate claim Htdef: t = add_SNo c (minus_SNo y).
Use reflexivity.
rewrite the current goal using Htdef (from left to right).
rewrite the current goal using Hneg2 (from left to right).
rewrite the current goal using Hcom (from left to right).
Use reflexivity.
rewrite the current goal using Hswap (from left to right).
An exact proof term for the current goal is HycLt.
We prove the intermediate claim HabsR: abs_SNo t ∈ R.
We prove the intermediate claim HtR: t ∈ R.
An exact proof term for the current goal is (real_add_SNo c HcR (minus_SNo y) (real_minus_SNo y HyR)).
An exact proof term for the current goal is (abs_SNo_in_R t HtR).
We prove the intermediate claim HabRlt: Rlt (abs_SNo t) r.
An exact proof term for the current goal is (RltI (abs_SNo t) r HabsR HrR Hablt).
We prove the intermediate claim HbdRlt: Rlt (R_bounded_distance c y) r.
Set ab to be the term abs_SNo t.
We prove the intermediate claim Hablt1: Rlt ab 1.
An exact proof term for the current goal is (Rlt_tra ab r 1 HabRlt Hrlt1R).
We prove the intermediate claim Hbddef: R_bounded_distance c y = If_i (Rlt ab 1) ab 1.
Use reflexivity.
We will prove Rlt (R_bounded_distance c y) r.
rewrite the current goal using Hbddef (from left to right).
rewrite the current goal using (If_i_1 (Rlt ab 1) ab 1 Hablt1) (from left to right).
An exact proof term for the current goal is HabRlt.
Apply (open_ballI R R_bounded_metric c r y HyR) to the current goal.
rewrite the current goal using (R_bounded_metric_apply c y HcR HyR) (from left to right).
An exact proof term for the current goal is HbdRlt.
∎