Let t be given.
Assume HtI: t ∈ closed_interval (minus_SNo 1) 1.
We will prove mul_SNo t two_thirds ∈ closed_interval (minus_SNo two_thirds) two_thirds.
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 H23R: two_thirds ∈ R.
An exact proof term for the current goal is two_thirds_in_R.
We prove the intermediate claim Hm23R: (minus_SNo two_thirds) ∈ R.
An exact proof term for the current goal is (real_minus_SNo two_thirds H23R).
We prove the intermediate claim HtR: t ∈ R.
An exact proof term for the current goal is (closed_interval_sub_R (minus_SNo 1) 1 t HtI).
We prove the intermediate claim HtS: SNo t.
An exact proof term for the current goal is (real_SNo t HtR).
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 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 Hbounds: Rle (minus_SNo 1) t ∧ Rle t 1.
An exact proof term for the current goal is (closed_interval_bounds (minus_SNo 1) 1 t Hm1R real_1 HtI).
We prove the intermediate claim HloRle: Rle (minus_SNo 1) t.
An exact proof term for the current goal is (andEL (Rle (minus_SNo 1) t) (Rle t 1) Hbounds).
We prove the intermediate claim HhiRle: Rle t 1.
An exact proof term for the current goal is (andER (Rle (minus_SNo 1) t) (Rle t 1) Hbounds).
We prove the intermediate claim Hnot_lt_lo: ¬ (t < (minus_SNo 1)).
Assume Hlt: t < (minus_SNo 1).
We prove the intermediate claim Hrlt: Rlt t (minus_SNo 1).
An exact proof term for the current goal is (RltI t (minus_SNo 1) HtR Hm1R Hlt).
An exact proof term for the current goal is ((RleE_nlt (minus_SNo 1) t HloRle) Hrlt).
We prove the intermediate claim Hnot_lt_hi: ¬ (1 < t).
Assume Hlt: 1 < t.
We prove the intermediate claim Hrlt: Rlt 1 t.
An exact proof term for the current goal is (RltI 1 t real_1 HtR Hlt).
An exact proof term for the current goal is ((RleE_nlt t 1 HhiRle) Hrlt).
We prove the intermediate claim Hm1_le_t: (minus_SNo 1) ≤ t.
Apply (SNoLtLe_or t (minus_SNo 1) HtS Hm1S) to the current goal.
Assume Hlt: t < (minus_SNo 1).
An exact proof term for the current goal is (FalseE (Hnot_lt_lo Hlt) ((minus_SNo 1) ≤ t)).
Assume Hle: (minus_SNo 1) ≤ t.
An exact proof term for the current goal is Hle.
We prove the intermediate claim Ht_le_1: t ≤ 1.
Apply (SNoLtLe_or 1 t SNo_1 HtS) to the current goal.
Assume Hlt: 1 < t.
An exact proof term for the current goal is (FalseE (Hnot_lt_hi Hlt) (t ≤ 1)).
Assume Hle: t ≤ 1.
An exact proof term for the current goal is Hle.
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 H0le_23: 0 ≤ two_thirds.
An exact proof term for the current goal is (SNoLtLe 0 two_thirds H23pos).
We prove the intermediate claim HmulR: mul_SNo t two_thirds ∈ R.
An exact proof term for the current goal is (real_mul_SNo t HtR two_thirds H23R).
We prove the intermediate claim HmulS: SNo (mul_SNo t two_thirds).
An exact proof term for the current goal is (real_SNo (mul_SNo t two_thirds) HmulR).
We prove the intermediate claim HloLe: mul_SNo (minus_SNo 1) two_thirds ≤ mul_SNo t two_thirds.
An exact proof term for the current goal is (nonneg_mul_SNo_Le' (minus_SNo 1) t two_thirds Hm1S HtS H23S H0le_23 Hm1_le_t).
We prove the intermediate claim HhiLe: mul_SNo t two_thirds ≤ mul_SNo 1 two_thirds.
An exact proof term for the current goal is (nonneg_mul_SNo_Le' t 1 two_thirds HtS SNo_1 H23S H0le_23 Ht_le_1).
We prove the intermediate claim HloR: mul_SNo (minus_SNo 1) two_thirds ∈ R.
An exact proof term for the current goal is (real_mul_SNo (minus_SNo 1) Hm1R two_thirds H23R).
We prove the intermediate claim HhiR: mul_SNo 1 two_thirds ∈ R.
An exact proof term for the current goal is (real_mul_SNo 1 real_1 two_thirds H23R).
We prove the intermediate claim HloRle': Rle (mul_SNo (minus_SNo 1) two_thirds) (mul_SNo t two_thirds).
An exact proof term for the current goal is (Rle_of_SNoLe (mul_SNo (minus_SNo 1) two_thirds) (mul_SNo t two_thirds) HloR HmulR HloLe).
We prove the intermediate claim HhiRle': Rle (mul_SNo t two_thirds) (mul_SNo 1 two_thirds).
An exact proof term for the current goal is (Rle_of_SNoLe (mul_SNo t two_thirds) (mul_SNo 1 two_thirds) HmulR HhiR HhiLe).
We prove the intermediate claim HloEq: 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) at position 1.
rewrite the current goal using (mul_SNo_oneL two_thirds H23S) (from left to right) at position 1.
Use reflexivity.
We prove the intermediate claim HhiEq: 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 Hm23le: Rle (minus_SNo two_thirds) (mul_SNo t two_thirds).
rewrite the current goal using HloEq (from right to left) at position 1.
An exact proof term for the current goal is HloRle'.
We prove the intermediate claim Hle23: Rle (mul_SNo t two_thirds) two_thirds.
rewrite the current goal using HhiEq (from right to left) at position 2.
An exact proof term for the current goal is HhiRle'.
An exact proof term for the current goal is (closed_intervalI_of_Rle (minus_SNo two_thirds) two_thirds (mul_SNo t two_thirds) Hm23R H23R HmulR Hm23le Hle23).
∎