Let c be given.
Assume HcR: c ∈ R.
Apply set_ext to the current goal.
Let y be given.
Assume HyB: y ∈ open_ball R R_bounded_metric c 1.
We will prove y ∈ open_interval (add_SNo c (minus_SNo 1)) (add_SNo c 1).
We prove the intermediate claim HdefI: open_interval (add_SNo c (minus_SNo 1)) (add_SNo c 1) = {x ∈ R|Rlt (add_SNo c (minus_SNo 1)) x ∧ Rlt x (add_SNo c 1)}.
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 1 y HyB).
We prove the intermediate claim Hdlt: Rlt (apply_fun R_bounded_metric (c,y)) 1.
An exact proof term for the current goal is (open_ballE2 R R_bounded_metric c 1 y HyB).
We prove the intermediate claim Hbdlt: Rlt (R_bounded_distance c y) 1.
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 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).
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 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) 1.
We prove the intermediate claim Hbddef: R_bounded_distance c y = If_i (Rlt (abs_SNo t) 1) (abs_SNo t) 1.
Use reflexivity.
We prove the intermediate claim HIfRlt: Rlt (If_i (Rlt (abs_SNo t) 1) (abs_SNo t) 1) 1.
rewrite the current goal using Hbddef (from right to left).
An exact proof term for the current goal is Hbdlt.
Apply (xm (Rlt (abs_SNo t) 1)) to the current goal.
Assume Hablt1: Rlt (abs_SNo t) 1.
rewrite the current goal using (If_i_1 (Rlt (abs_SNo t) 1) (abs_SNo t) 1 Hablt1) (from right to left).
An exact proof term for the current goal is HIfRlt.
Assume Hnablt1: ¬ (Rlt (abs_SNo t) 1).
We prove the intermediate claim H1lt: Rlt 1 1.
rewrite the current goal using (If_i_0 (Rlt (abs_SNo t) 1) (abs_SNo t) 1 Hnablt1) (from right to left) at position 1.
An exact proof term for the current goal is HIfRlt.
An exact proof term for the current goal is (FalseE ((not_Rlt_refl 1 real_1) H1lt) (Rlt (abs_SNo t) 1)).
We prove the intermediate claim Hablt: abs_SNo t < 1.
An exact proof term for the current goal is (RltE_lt (abs_SNo t) 1 HabRlt).
We prove the intermediate claim H1S: SNo 1.
An exact proof term for the current goal is SNo_1.
We prove the intermediate claim Htlt: t < 1.
An exact proof term for the current goal is (abs_SNo_lt_imp_lt t 1 HtS H1S SNoLt_0_1 Hablt).
We prove the intermediate claim Hmtlt: minus_SNo t < 1.
An exact proof term for the current goal is (abs_SNo_lt_imp_neg_lt t 1 HtS H1S SNoLt_0_1 Hablt).
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) < 1.
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 1.
We prove the intermediate claim Hlt1: y < add_SNo 1 c.
An exact proof term for the current goal is (add_SNo_minus_Lt1 y c 1 HyS HcS SNo_1 HycLt).
We prove the intermediate claim Hcom: add_SNo 1 c = add_SNo c 1.
An exact proof term for the current goal is (add_SNo_com 1 c SNo_1 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 1) < y.
We prove the intermediate claim Hlt1: c < add_SNo 1 y.
An exact proof term for the current goal is (add_SNo_minus_Lt1 c y 1 HcS HyS SNo_1 Htlt).
We prove the intermediate claim Hcom1: add_SNo 1 y = add_SNo y 1.
An exact proof term for the current goal is (add_SNo_com 1 y SNo_1 HyS).
We prove the intermediate claim Hlt2: c < add_SNo y 1.
rewrite the current goal using Hcom1 (from right to left).
An exact proof term for the current goal is Hlt1.
An exact proof term for the current goal is (add_SNo_minus_Lt1b c 1 y HcS SNo_1 HyS Hlt2).
We prove the intermediate claim HclR: add_SNo c (minus_SNo 1) ∈ R.
An exact proof term for the current goal is (real_add_SNo c HcR (minus_SNo 1) (real_minus_SNo 1 real_1)).
We prove the intermediate claim HcrR: 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 HleftRlt: Rlt (add_SNo c (minus_SNo 1)) y.
An exact proof term for the current goal is (RltI (add_SNo c (minus_SNo 1)) y HclR HyR HcmyLt).
We prove the intermediate claim HrightRlt: Rlt y (add_SNo c 1).
An exact proof term for the current goal is (RltI y (add_SNo c 1) HyR HcrR HyLt).
An exact proof term for the current goal is (SepI R (λx0 : set ⇒ Rlt (add_SNo c (minus_SNo 1)) x0 ∧ Rlt x0 (add_SNo c 1)) y HyR (andI (Rlt (add_SNo c (minus_SNo 1)) y) (Rlt y (add_SNo c 1)) HleftRlt HrightRlt)).
Let y be given.
Assume HyI: y ∈ open_interval (add_SNo c (minus_SNo 1)) (add_SNo c 1).
We will prove y ∈ open_ball R R_bounded_metric c 1.
We prove the intermediate claim HdefI: open_interval (add_SNo c (minus_SNo 1)) (add_SNo c 1) = {x ∈ R|Rlt (add_SNo c (minus_SNo 1)) x ∧ Rlt x (add_SNo c 1)}.
Use reflexivity.
We prove the intermediate claim HyI': y ∈ {x ∈ R|Rlt (add_SNo c (minus_SNo 1)) x ∧ Rlt x (add_SNo c 1)}.
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 1)) x0 ∧ Rlt x0 (add_SNo c 1)) y HyI').
We prove the intermediate claim Hconj: Rlt (add_SNo c (minus_SNo 1)) y ∧ Rlt y (add_SNo c 1).
An exact proof term for the current goal is (SepE2 R (λx0 : set ⇒ Rlt (add_SNo c (minus_SNo 1)) x0 ∧ Rlt x0 (add_SNo c 1)) y HyI').
We prove the intermediate claim Hleft: Rlt (add_SNo c (minus_SNo 1)) y.
An exact proof term for the current goal is (andEL (Rlt (add_SNo c (minus_SNo 1)) y) (Rlt y (add_SNo c 1)) Hconj).
We prove the intermediate claim Hright: Rlt y (add_SNo c 1).
An exact proof term for the current goal is (andER (Rlt (add_SNo c (minus_SNo 1)) y) (Rlt y (add_SNo c 1)) 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).
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 HycLt: add_SNo y (minus_SNo c) < 1.
We prove the intermediate claim HltY: y < add_SNo c 1.
An exact proof term for the current goal is (RltE_lt y (add_SNo c 1) Hright).
We prove the intermediate claim Hcom: add_SNo c 1 = add_SNo 1 c.
An exact proof term for the current goal is (add_SNo_com c 1 HcS SNo_1).
We prove the intermediate claim Hlt2: y < add_SNo 1 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 1 HyS HcS SNo_1 Hlt2).
We prove the intermediate claim HcyLt: add_SNo c (minus_SNo y) < 1.
We prove the intermediate claim Hcylt: add_SNo c (minus_SNo 1) < y.
An exact proof term for the current goal is (RltE_lt (add_SNo c (minus_SNo 1)) y Hleft).
We prove the intermediate claim Hsum: add_SNo 1 (add_SNo c (minus_SNo 1)) < add_SNo 1 y.
An exact proof term for the current goal is (add_SNo_Lt2 1 (add_SNo c (minus_SNo 1)) y SNo_1 (SNo_add_SNo c (minus_SNo 1) HcS (SNo_minus_SNo 1 SNo_1)) HyS Hcylt).
We prove the intermediate claim Heqleft: add_SNo 1 (add_SNo c (minus_SNo 1)) = c.
rewrite the current goal using (add_SNo_assoc 1 c (minus_SNo 1) SNo_1 HcS (SNo_minus_SNo 1 SNo_1)) (from left to right).
rewrite the current goal using (add_SNo_com 1 c SNo_1 HcS) (from left to right).
rewrite the current goal using (add_SNo_assoc c 1 (minus_SNo 1) HcS SNo_1 (SNo_minus_SNo 1 SNo_1)) (from right to left).
rewrite the current goal using (add_SNo_minus_SNo_rinv 1 SNo_1) (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 1 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 1 HcS HyS SNo_1 Hlt3).
We prove the intermediate claim Hablt: abs_SNo t < 1.
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 prove the intermediate claim Htdef: t = add_SNo c (minus_SNo y).
Use reflexivity.
We will prove minus_SNo t = add_SNo y (minus_SNo c).
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) 1.
An exact proof term for the current goal is (RltI (abs_SNo t) 1 HabsR real_1 Hablt).
We prove the intermediate claim HbdRlt: Rlt (R_bounded_distance c y) 1.
We prove the intermediate claim Hbddef: R_bounded_distance c y = If_i (Rlt (abs_SNo t) 1) (abs_SNo t) 1.
Use reflexivity.
rewrite the current goal using Hbddef (from left to right).
rewrite the current goal using (If_i_1 (Rlt (abs_SNo t) 1) (abs_SNo t) 1 HabRlt) (from left to right).
An exact proof term for the current goal is HabRlt.
Apply (open_ballI R R_bounded_metric c 1 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.
∎