Let a and b be given.
Assume HaI: a ∈ unit_interval.
Assume HbI: b ∈ unit_interval.
We will prove mul_SNo a b ∈ unit_interval.
We prove the intermediate claim HaR: a ∈ R.
An exact proof term for the current goal is (unit_interval_sub_R a HaI).
We prove the intermediate claim HbR: b ∈ R.
An exact proof term for the current goal is (unit_interval_sub_R b HbI).
We prove the intermediate claim HaS: SNo a.
An exact proof term for the current goal is (real_SNo a HaR).
We prove the intermediate claim HbS: SNo b.
An exact proof term for the current goal is (real_SNo b HbR).
We prove the intermediate claim Ha0: Rle 0 a.
An exact proof term for the current goal is (unit_interval_Rle0 a HaI).
We prove the intermediate claim Hb0: Rle 0 b.
An exact proof term for the current goal is (unit_interval_Rle0 b HbI).
We prove the intermediate claim Ha1: Rle a 1.
An exact proof term for the current goal is (unit_interval_Rle1 a HaI).
We prove the intermediate claim Hb1: Rle b 1.
An exact proof term for the current goal is (unit_interval_Rle1 b HbI).
We prove the intermediate claim Ha0S: 0 ≤ a.
An exact proof term for the current goal is (SNoLe_of_Rle 0 a Ha0).
We prove the intermediate claim Hb0S: 0 ≤ b.
An exact proof term for the current goal is (SNoLe_of_Rle 0 b Hb0).
We prove the intermediate claim Ha1S: a ≤ 1.
An exact proof term for the current goal is (SNoLe_of_Rle a 1 Ha1).
We prove the intermediate claim Hb1S: b ≤ 1.
An exact proof term for the current goal is (SNoLe_of_Rle b 1 Hb1).
We prove the intermediate claim HabR: mul_SNo a b ∈ R.
An exact proof term for the current goal is (real_mul_SNo a HaR b HbR).
We prove the intermediate claim HabS: SNo (mul_SNo a b).
An exact proof term for the current goal is (real_SNo (mul_SNo a b) HabR).
We prove the intermediate claim H0leabS: 0 ≤ mul_SNo a b.
An exact proof term for the current goal is (mul_SNo_nonneg_nonneg a b HaS HbS Ha0S Hb0S).
We prove the intermediate claim HabLeB: mul_SNo a b ≤ b.
An exact proof term for the current goal is (mul_SNo_Le1_nonneg_Le a b HaS HbS Ha1S Hb0S).
We prove the intermediate claim HabLe1S: mul_SNo a b ≤ 1.
An exact proof term for the current goal is (SNoLe_tra (mul_SNo a b) b 1 HabS HbS SNo_1 HabLeB Hb1S).
Apply (SepI R (λt : set ⇒ ¬ (Rlt t 0) ∧ ¬ (Rlt 1 t)) (mul_SNo a b) HabR) to the current goal.
Apply andI to the current goal.
Assume Hablt0: Rlt (mul_SNo a b) 0.
We will prove False.
We prove the intermediate claim Hablt0S: mul_SNo a b < 0.
An exact proof term for the current goal is (RltE_lt (mul_SNo a b) 0 Hablt0).
We prove the intermediate claim H00: 0 < 0.
An exact proof term for the current goal is (SNoLeLt_tra 0 (mul_SNo a b) 0 SNo_0 HabS SNo_0 H0leabS Hablt0S).
An exact proof term for the current goal is ((SNoLt_irref 0) H00).
Assume H1ltab: Rlt 1 (mul_SNo a b).
We will prove False.
We prove the intermediate claim H1ltabS: 1 < mul_SNo a b.
An exact proof term for the current goal is (RltE_lt 1 (mul_SNo a b) H1ltab).
We prove the intermediate claim H1leabS: 1 ≤ mul_SNo a b.
An exact proof term for the current goal is (SNoLtLe 1 (mul_SNo a b) H1ltabS).
We prove the intermediate claim HabEq1: mul_SNo a b = 1.
An exact proof term for the current goal is (SNoLe_antisym (mul_SNo a b) 1 HabS SNo_1 HabLe1S H1leabS).
We prove the intermediate claim H11: 1 < 1.
rewrite the current goal using HabEq1 (from right to left) at position 2.
An exact proof term for the current goal is H1ltabS.
An exact proof term for the current goal is ((SNoLt_irref 1) H11).
∎