Let t and c be given.
Assume HtI: t ∈ closed_interval (minus_SNo 1) 1.
Assume HcR: c ∈ R.
Assume H0leC: 0 ≤ c.
We will prove mul_SNo t c ∈ closed_interval (minus_SNo c) c.
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 HmcR: minus_SNo c ∈ R.
An exact proof term for the current goal is (real_minus_SNo c HcR).
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 HcS: SNo c.
An exact proof term for the current goal is (real_SNo c HcR).
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 HmulR: mul_SNo t c ∈ R.
An exact proof term for the current goal is (real_mul_SNo t HtR c HcR).
We prove the intermediate claim HmulS: SNo (mul_SNo t c).
An exact proof term for the current goal is (real_SNo (mul_SNo t c) HmulR).
We prove the intermediate claim HloLe: mul_SNo (minus_SNo 1) c ≤ mul_SNo t c.
An exact proof term for the current goal is (nonneg_mul_SNo_Le' (minus_SNo 1) t c Hm1S HtS HcS H0leC Hm1_le_t).
We prove the intermediate claim HhiLe: mul_SNo t c ≤ mul_SNo 1 c.
An exact proof term for the current goal is (nonneg_mul_SNo_Le' t 1 c HtS SNo_1 HcS H0leC Ht_le_1).
We prove the intermediate claim HloR: mul_SNo (minus_SNo 1) c ∈ R.
An exact proof term for the current goal is (real_mul_SNo (minus_SNo 1) Hm1R c HcR).
We prove the intermediate claim HhiR: mul_SNo 1 c ∈ R.
An exact proof term for the current goal is (real_mul_SNo 1 real_1 c HcR).
We prove the intermediate claim HloRle': Rle (mul_SNo (minus_SNo 1) c) (mul_SNo t c).
An exact proof term for the current goal is (Rle_of_SNoLe (mul_SNo (minus_SNo 1) c) (mul_SNo t c) HloR HmulR HloLe).
We prove the intermediate claim HhiRle': Rle (mul_SNo t c) (mul_SNo 1 c).
An exact proof term for the current goal is (Rle_of_SNoLe (mul_SNo t c) (mul_SNo 1 c) HmulR HhiR HhiLe).
We prove the intermediate claim HloEq: mul_SNo (minus_SNo 1) c = minus_SNo c.
rewrite the current goal using (mul_SNo_minus_distrL 1 c SNo_1 HcS) (from left to right) at position 1.
rewrite the current goal using (mul_SNo_oneL c HcS) (from left to right) at position 1.
Use reflexivity.
We prove the intermediate claim HhiEq: mul_SNo 1 c = c.
An exact proof term for the current goal is (mul_SNo_oneL c HcS).
We prove the intermediate claim Hmc_le: Rle (minus_SNo c) (mul_SNo t c).
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 Hle_c: Rle (mul_SNo t c) c.
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 c) c (mul_SNo t c) HmcR HcR HmulR Hmc_le Hle_c).
∎