Let t be given.
Assume HtL: t ∈ unit_interval_left_half.
We will prove apply_fun double_map_left_half t ∈ unit_interval.
rewrite the current goal using (double_map_apply t HtL) (from left to right).
We will prove mul_SNo 2 t ∈ unit_interval.
We prove the intermediate claim HtI: t ∈ unit_interval.
An exact proof term for the current goal is (unit_interval_left_half_sub t HtL).
We prove the intermediate claim HtR: t ∈ R.
An exact proof term for the current goal is (unit_interval_sub_R 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 H2R: 2 ∈ R.
An exact proof term for the current goal is two_in_R.
We prove the intermediate claim HmulR: mul_SNo 2 t ∈ R.
An exact proof term for the current goal is (real_mul_SNo 2 H2R t HtR).
Apply (SepI R (λs : set ⇒ ¬ (Rlt s 0) ∧ ¬ (Rlt 1 s)) (mul_SNo 2 t) HmulR) to the current goal.
Apply andI to the current goal.
Assume Hlt: Rlt (mul_SNo 2 t) 0.
We will prove False.
We prove the intermediate claim H2S: SNo 2.
An exact proof term for the current goal is SNo_2.
We prove the intermediate claim HmulS: SNo (mul_SNo 2 t).
An exact proof term for the current goal is (SNo_mul_SNo 2 t H2S HtS).
We prove the intermediate claim Ht0nlt: ¬ (Rlt t 0).
We prove the intermediate claim Hconj: ¬ (Rlt t 0) ∧ ¬ (Rlt 1 t).
An exact proof term for the current goal is (SepE2 R (λu : set ⇒ ¬ (Rlt u 0) ∧ ¬ (Rlt 1 u)) t HtI).
An exact proof term for the current goal is (andEL (¬ (Rlt t 0)) (¬ (Rlt 1 t)) Hconj).
We prove the intermediate claim H0le2: 0 ≤ 2.
An exact proof term for the current goal is (SNoLtLe 0 2 SNoLt_0_2).
We prove the intermediate claim H0let: 0 ≤ t.
We will prove 0 ≤ t.
Apply (SNoLtLe_or t 0 HtS SNo_0) to the current goal.
Assume Htlt0: t < 0.
We prove the intermediate claim Hrtlt: Rlt t 0.
An exact proof term for the current goal is (RltI t 0 HtR real_0 Htlt0).
Apply FalseE to the current goal.
An exact proof term for the current goal is (Ht0nlt Hrtlt).
Assume H0let': 0 ≤ t.
An exact proof term for the current goal is H0let'.
We prove the intermediate claim H0lemul: 0 ≤ mul_SNo 2 t.
An exact proof term for the current goal is (mul_SNo_nonneg_nonneg 2 t H2S HtS H0le2 H0let).
We prove the intermediate claim HmulLt0: mul_SNo 2 t < 0.
An exact proof term for the current goal is (RltE_lt (mul_SNo 2 t) 0 Hlt).
We prove the intermediate claim Hcases: 0 < (mul_SNo 2 t) ∨ 0 = (mul_SNo 2 t).
An exact proof term for the current goal is (SNoLeE 0 (mul_SNo 2 t) SNo_0 HmulS H0lemul).
Apply Hcases to the current goal.
Assume Hpos: 0 < (mul_SNo 2 t).
We prove the intermediate claim H00: 0 < 0.
An exact proof term for the current goal is (SNoLt_tra 0 (mul_SNo 2 t) 0 SNo_0 HmulS SNo_0 Hpos HmulLt0).
An exact proof term for the current goal is ((SNoLt_irref 0) H00).
Assume Heq: 0 = (mul_SNo 2 t).
We prove the intermediate claim H00: 0 < 0.
rewrite the current goal using Heq (from left to right) at position 1.
An exact proof term for the current goal is HmulLt0.
An exact proof term for the current goal is ((SNoLt_irref 0) H00).
Assume Hlt: Rlt 1 (mul_SNo 2 t).
We will prove False.
We prove the intermediate claim H2S: SNo 2.
An exact proof term for the current goal is SNo_2.
We prove the intermediate claim HmulS: SNo (mul_SNo 2 t).
An exact proof term for the current goal is (SNo_mul_SNo 2 t H2S HtS).
We prove the intermediate claim HeS: SNo (eps_ 1).
An exact proof term for the current goal is (real_SNo (eps_ 1) eps_1_in_R).
We prove the intermediate claim Hnlt: ¬ (Rlt (eps_ 1) t).
An exact proof term for the current goal is (SepE2 unit_interval (λu : set ⇒ ¬ (Rlt (eps_ 1) u)) t HtL).
We prove the intermediate claim Htle: t ≤ (eps_ 1).
We will prove t ≤ (eps_ 1).
Apply (SNoLtLe_or (eps_ 1) t HeS HtS) to the current goal.
Assume Hepslt: (eps_ 1) < t.
We prove the intermediate claim Hrtlt: Rlt (eps_ 1) t.
An exact proof term for the current goal is (RltI (eps_ 1) t eps_1_in_R HtR Hepslt).
Apply FalseE to the current goal.
An exact proof term for the current goal is (Hnlt Hrtlt).
Assume Htle': t ≤ (eps_ 1).
An exact proof term for the current goal is Htle'.
We prove the intermediate claim H0le2: 0 ≤ 2.
An exact proof term for the current goal is (SNoLtLe 0 2 SNoLt_0_2).
We prove the intermediate claim H2tLe: mul_SNo 2 t ≤ 1.
We prove the intermediate claim H2eps: mul_SNo 2 t ≤ mul_SNo 2 (eps_ 1).
An exact proof term for the current goal is (nonneg_mul_SNo_Le 2 t (eps_ 1) H2S H0le2 HtS HeS Htle).
We will prove mul_SNo 2 t ≤ 1.
rewrite the current goal using eps_1_half_eq2 (from right to left) at position 2.
An exact proof term for the current goal is H2eps.
We prove the intermediate claim H1lt: 1 < (mul_SNo 2 t).
An exact proof term for the current goal is (RltE_lt 1 (mul_SNo 2 t) Hlt).
We prove the intermediate claim Hcases: (mul_SNo 2 t) < 1 ∨ (mul_SNo 2 t) = 1.
An exact proof term for the current goal is (SNoLeE (mul_SNo 2 t) 1 HmulS SNo_1 H2tLe).
Apply Hcases to the current goal.
Assume Hlt2: (mul_SNo 2 t) < 1.
We prove the intermediate claim H11: 1 < 1.
An exact proof term for the current goal is (SNoLt_tra 1 (mul_SNo 2 t) 1 SNo_1 HmulS SNo_1 H1lt Hlt2).
An exact proof term for the current goal is ((SNoLt_irref 1) H11).
Assume Heq: (mul_SNo 2 t) = 1.
We prove the intermediate claim H11: 1 < 1.
rewrite the current goal using Heq (from right to left) at position 2.
An exact proof term for the current goal is H1lt.
An exact proof term for the current goal is ((SNoLt_irref 1) H11).
∎