Let t be given.
Assume HtI: t ∈ closed_interval (minus_SNo two_thirds) two_thirds.
We will prove div_SNo t two_thirds ∈ closed_interval (minus_SNo 1) 1.
We prove the intermediate claim H23R: two_thirds ∈ R.
An exact proof term for the current goal is two_thirds_in_R.
We prove the intermediate claim H23S: SNo two_thirds.
An exact proof term for the current goal is (real_SNo two_thirds H23R).
We prove the intermediate claim H23pos: 0 < two_thirds.
An exact proof term for the current goal is two_thirds_pos.
We prove the intermediate claim HtR: t ∈ R.
An exact proof term for the current goal is (closed_interval_sub_R (minus_SNo two_thirds) two_thirds t HtI).
We prove the intermediate claim HtS: SNo t.
An exact proof term for the current goal is (real_SNo t HtR).
Set u to be the term div_SNo t two_thirds.
We prove the intermediate claim HuS: SNo u.
We prove the intermediate claim HuEq: u = div_SNo t two_thirds.
Use reflexivity.
rewrite the current goal using HuEq (from left to right).
An exact proof term for the current goal is (SNo_div_SNo t two_thirds HtS H23S).
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 HuR: u ∈ R.
An exact proof term for the current goal is (real_div_SNo t HtR two_thirds H23R).
We prove the intermediate claim HcasesCI: u ∈ closed_interval (minus_SNo 1) 1 ∨ ¬ (u ∈ closed_interval (minus_SNo 1) 1).
An exact proof term for the current goal is (xm (u ∈ closed_interval (minus_SNo 1) 1)).
Apply HcasesCI to the current goal.
Assume HuCI: u ∈ closed_interval (minus_SNo 1) 1.
An exact proof term for the current goal is HuCI.
Assume Hnot: ¬ (u ∈ closed_interval (minus_SNo 1) 1).
Apply FalseE to the current goal.
We prove the intermediate claim Hcases: Rlt u (minus_SNo 1) ∨ Rlt 1 u.
An exact proof term for the current goal is (closed_interval_not_mem_cases (minus_SNo 1) 1 u Hm1R real_1 HuR Hnot).
Apply Hcases to the current goal.
Assume Hltm1: Rlt u (minus_SNo 1).
We prove the intermediate claim Hltm1S: u < (minus_SNo 1).
An exact proof term for the current goal is (RltE_lt u (minus_SNo 1) Hltm1).
We prove the intermediate claim Hm1S: SNo (minus_SNo 1).
An exact proof term for the current goal is (SNo_minus_SNo 1 SNo_1).
We prove the intermediate claim HmulLtS: mul_SNo u two_thirds < mul_SNo (minus_SNo 1) two_thirds.
An exact proof term for the current goal is (pos_mul_SNo_Lt' u (minus_SNo 1) two_thirds HuS Hm1S H23S H23pos Hltm1S).
We prove the intermediate claim HmulLtS2: mul_SNo two_thirds u < mul_SNo (minus_SNo 1) two_thirds.
rewrite the current goal using (mul_SNo_com u two_thirds HuS H23S) (from right to left) at position 1.
An exact proof term for the current goal is HmulLtS.
We prove the intermediate claim H23ne0: two_thirds ≠ 0.
An exact proof term for the current goal is two_thirds_ne0.
We prove the intermediate claim HmulEq: mul_SNo two_thirds u = t.
We prove the intermediate claim HtuEq: u = div_SNo t two_thirds.
Use reflexivity.
rewrite the current goal using HtuEq (from left to right).
An exact proof term for the current goal is (mul_div_SNo_invR t two_thirds HtS H23S H23ne0).
We prove the intermediate claim Hm1mulEq: mul_SNo (minus_SNo 1) two_thirds = minus_SNo two_thirds.
rewrite the current goal using (mul_SNo_minus_distrL 1 two_thirds SNo_1 H23S) (from left to right).
rewrite the current goal using (mul_SNo_oneL two_thirds H23S) (from left to right).
Use reflexivity.
We prove the intermediate claim HtLtS: t < minus_SNo two_thirds.
rewrite the current goal using HmulEq (from right to left) at position 1.
rewrite the current goal using Hm1mulEq (from right to left).
An exact proof term for the current goal is HmulLtS2.
We prove the intermediate claim HtLt: Rlt t (minus_SNo two_thirds).
An exact proof term for the current goal is (RltI t (minus_SNo two_thirds) HtR (real_minus_SNo two_thirds H23R) HtLtS).
We prove the intermediate claim Hbounds: Rle (minus_SNo two_thirds) t ∧ Rle t two_thirds.
An exact proof term for the current goal is (closed_interval_bounds (minus_SNo two_thirds) two_thirds t (real_minus_SNo two_thirds H23R) H23R HtI).
We prove the intermediate claim Hm23le_t: Rle (minus_SNo two_thirds) t.
An exact proof term for the current goal is (andEL (Rle (minus_SNo two_thirds) t) (Rle t two_thirds) Hbounds).
An exact proof term for the current goal is ((RleE_nlt (minus_SNo two_thirds) t Hm23le_t) HtLt).
Assume Hu1lt: Rlt 1 u.
We prove the intermediate claim Hu1ltS: 1 < u.
An exact proof term for the current goal is (RltE_lt 1 u Hu1lt).
We prove the intermediate claim H1S: SNo 1.
An exact proof term for the current goal is SNo_1.
We prove the intermediate claim HmulLtS: mul_SNo 1 two_thirds < mul_SNo u two_thirds.
An exact proof term for the current goal is (pos_mul_SNo_Lt' 1 u two_thirds H1S HuS H23S H23pos Hu1ltS).
We prove the intermediate claim H23ne0: two_thirds ≠ 0.
An exact proof term for the current goal is two_thirds_ne0.
We prove the intermediate claim HmulEq: mul_SNo two_thirds u = t.
We prove the intermediate claim HtuEq: u = div_SNo t two_thirds.
Use reflexivity.
rewrite the current goal using HtuEq (from left to right).
An exact proof term for the current goal is (mul_div_SNo_invR t two_thirds HtS H23S H23ne0).
We prove the intermediate claim H1mulEq: mul_SNo 1 two_thirds = two_thirds.
An exact proof term for the current goal is (mul_SNo_oneL two_thirds H23S).
We prove the intermediate claim HmulLtS2: mul_SNo 1 two_thirds < mul_SNo two_thirds u.
rewrite the current goal using (mul_SNo_com u two_thirds HuS H23S) (from right to left).
An exact proof term for the current goal is HmulLtS.
We prove the intermediate claim HtGtS: two_thirds < t.
rewrite the current goal using H1mulEq (from right to left) at position 1.
rewrite the current goal using HmulEq (from right to left).
An exact proof term for the current goal is HmulLtS2.
We prove the intermediate claim HtGt: Rlt two_thirds t.
An exact proof term for the current goal is (RltI two_thirds t H23R HtR HtGtS).
We prove the intermediate claim Hbounds: Rle (minus_SNo two_thirds) t ∧ Rle t two_thirds.
An exact proof term for the current goal is (closed_interval_bounds (minus_SNo two_thirds) two_thirds t (real_minus_SNo two_thirds H23R) H23R HtI).
We prove the intermediate claim Ht_le_23: Rle t two_thirds.
An exact proof term for the current goal is (andER (Rle (minus_SNo two_thirds) t) (Rle t two_thirds) Hbounds).
An exact proof term for the current goal is ((RleE_nlt t two_thirds Ht_le_23) HtGt).
∎