Let den and y be given.
Assume HdenR: den ∈ R.
Assume HdenPos: 0 < den.
Assume HyI2: y ∈ closed_interval (minus_SNo den) den.
We will prove div_SNo y den ∈ closed_interval (minus_SNo 1) 1.
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 HmdenR: (minus_SNo den) ∈ R.
An exact proof term for the current goal is (real_minus_SNo den HdenR).
We prove the intermediate claim HyR: y ∈ R.
An exact proof term for the current goal is (closed_interval_sub_R (minus_SNo den) den y HyI2).
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 HdenS: SNo den.
An exact proof term for the current goal is (real_SNo den HdenR).
We prove the intermediate claim Hdenne0: den ≠ 0.
An exact proof term for the current goal is (SNo_pos_ne0 den HdenS HdenPos).
We prove the intermediate claim Hbounds: Rle (minus_SNo den) y ∧ Rle y den.
An exact proof term for the current goal is (closed_interval_bounds (minus_SNo den) den y HmdenR HdenR HyI2).
We prove the intermediate claim Hlo: Rle (minus_SNo den) y.
An exact proof term for the current goal is (andEL (Rle (minus_SNo den) y) (Rle y den) Hbounds).
We prove the intermediate claim Hhi: Rle y den.
An exact proof term for the current goal is (andER (Rle (minus_SNo den) y) (Rle y den) Hbounds).
We prove the intermediate claim Hnlt_hi: ¬ (Rlt den y).
An exact proof term for the current goal is (RleE_nlt y den Hhi).
We prove the intermediate claim Hnlt_lo: ¬ (Rlt y (minus_SNo den)).
An exact proof term for the current goal is (RleE_nlt (minus_SNo den) y Hlo).
We prove the intermediate claim HyDivR: div_SNo y den ∈ R.
An exact proof term for the current goal is (real_div_SNo y HyR den HdenR).
We prove the intermediate claim HyDivS: SNo (div_SNo y den).
An exact proof term for the current goal is (real_SNo (div_SNo y den) HyDivR).
We prove the intermediate claim Hy_le_1: Rle (div_SNo y den) 1.
Apply (RleI (div_SNo y den) 1 HyDivR real_1) to the current goal.
We will prove ¬ (Rlt 1 (div_SNo y den)).
Assume H1lt: Rlt 1 (div_SNo y den).
We prove the intermediate claim H1lty: 1 < div_SNo y den.
An exact proof term for the current goal is (RltE_lt 1 (div_SNo y den) H1lt).
We prove the intermediate claim HmulLt: mul_SNo 1 den < mul_SNo (div_SNo y den) den.
An exact proof term for the current goal is (pos_mul_SNo_Lt' 1 (div_SNo y den) den SNo_1 HyDivS HdenS HdenPos H1lty).
We prove the intermediate claim HmulLt': den < mul_SNo (div_SNo y den) den.
rewrite the current goal using (mul_SNo_oneL den HdenS) (from right to left) at position 1.
An exact proof term for the current goal is HmulLt.
We prove the intermediate claim HmulEq: mul_SNo (div_SNo y den) den = y.
An exact proof term for the current goal is (mul_div_SNo_invL y den HyS HdenS Hdenne0).
We prove the intermediate claim Hden_lt_y: den < y.
rewrite the current goal using HmulEq (from right to left).
An exact proof term for the current goal is HmulLt'.
We prove the intermediate claim Hbad: Rlt den y.
An exact proof term for the current goal is (RltI den y HdenR HyR Hden_lt_y).
An exact proof term for the current goal is (Hnlt_hi Hbad).
We prove the intermediate claim Hm1_le_y: Rle (minus_SNo 1) (div_SNo y den).
Apply (RleI (minus_SNo 1) (div_SNo y den) Hm1R HyDivR) to the current goal.
We will prove ¬ (Rlt (div_SNo y den) (minus_SNo 1)).
Assume Hylt: Rlt (div_SNo y den) (minus_SNo 1).
We prove the intermediate claim Hylts: div_SNo y den < minus_SNo 1.
An exact proof term for the current goal is (RltE_lt (div_SNo y den) (minus_SNo 1) Hylt).
We prove the intermediate claim HmulLt: mul_SNo (div_SNo y den) den < mul_SNo (minus_SNo 1) den.
An exact proof term for the current goal is (pos_mul_SNo_Lt' (div_SNo y den) (minus_SNo 1) den HyDivS (SNo_minus_SNo 1 SNo_1) HdenS HdenPos Hylts).
We prove the intermediate claim HmulEq: mul_SNo (div_SNo y den) den = y.
An exact proof term for the current goal is (mul_div_SNo_invL y den HyS HdenS Hdenne0).
We prove the intermediate claim HrhsEq: mul_SNo (minus_SNo 1) den = minus_SNo den.
rewrite the current goal using (mul_SNo_minus_distrL 1 den SNo_1 HdenS) (from left to right) at position 1.
rewrite the current goal using (mul_SNo_oneL den HdenS) (from left to right) at position 1.
Use reflexivity.
We prove the intermediate claim Hy_lt_mden: y < minus_SNo den.
rewrite the current goal using HmulEq (from right to left).
rewrite the current goal using HrhsEq (from right to left).
An exact proof term for the current goal is HmulLt.
We prove the intermediate claim Hbad: Rlt y (minus_SNo den).
An exact proof term for the current goal is (RltI y (minus_SNo den) HyR HmdenR Hy_lt_mden).
An exact proof term for the current goal is (Hnlt_lo Hbad).
An exact proof term for the current goal is (closed_intervalI_of_Rle (minus_SNo 1) 1 (div_SNo y den) Hm1R real_1 HyDivR Hm1_le_y Hy_le_1).
∎