Let t be given.
Assume HtH: t ∈ unit_interval_right_half.
We will prove apply_fun double_minus_one_map_right_half t ∈ unit_interval.
rewrite the current goal using (double_minus_one_map_apply t HtH) (from left to right).
We will prove add_SNo (mul_SNo 2 t) (minus_SNo 1) ∈ unit_interval.
We prove the intermediate claim HtI: t ∈ unit_interval.
An exact proof term for the current goal is (unit_interval_right_half_sub t HtH).
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 HeR: eps_ 1 ∈ R.
An exact proof term for the current goal is eps_1_in_R.
We prove the intermediate claim HeS: SNo (eps_ 1).
An exact proof term for the current goal is (real_SNo (eps_ 1) HeR).
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 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 Hm1S: SNo (minus_SNo 1).
An exact proof term for the current goal is (real_SNo (minus_SNo 1) Hm1R).
We prove the intermediate claim H2S: SNo 2.
An exact proof term for the current goal is SNo_2.
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).
We prove the intermediate claim HsR: add_SNo (mul_SNo 2 t) (minus_SNo 1) ∈ R.
An exact proof term for the current goal is (real_add_SNo (mul_SNo 2 t) HmulR (minus_SNo 1) Hm1R).
We prove the intermediate claim HsS: SNo (add_SNo (mul_SNo 2 t) (minus_SNo 1)).
An exact proof term for the current goal is (real_SNo (add_SNo (mul_SNo 2 t) (minus_SNo 1)) HsR).
Apply (SepI R (λu : set ⇒ ¬ (Rlt u 0) ∧ ¬ (Rlt 1 u)) (add_SNo (mul_SNo 2 t) (minus_SNo 1)) HsR) to the current goal.
Apply andI to the current goal.
Assume Hlt: Rlt (add_SNo (mul_SNo 2 t) (minus_SNo 1)) 0.
We will prove False.
We prove the intermediate claim Hslt0: add_SNo (mul_SNo 2 t) (minus_SNo 1) < 0.
An exact proof term for the current goal is (RltE_lt (add_SNo (mul_SNo 2 t) (minus_SNo 1)) 0 Hlt).
We prove the intermediate claim Hnlt_t_eps: ¬ (Rlt t (eps_ 1)).
An exact proof term for the current goal is (SepE2 unit_interval (λu : set ⇒ ¬ (Rlt u (eps_ 1))) t HtH).
We prove the intermediate claim Hepsle_t: (eps_ 1) ≤ t.
We will prove (eps_ 1) ≤ t.
Apply (SNoLtLe_or t (eps_ 1) HtS HeS) to the current goal.
Assume Htlt: t < (eps_ 1).
We prove the intermediate claim Hrlt: Rlt t (eps_ 1).
An exact proof term for the current goal is (RltI t (eps_ 1) HtR HeR Htlt).
Apply FalseE to the current goal.
An exact proof term for the current goal is (Hnlt_t_eps Hrlt).
Assume Hle: (eps_ 1) ≤ t.
An exact proof term for the current goal is Hle.
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 H2eps_le_2t: mul_SNo 2 (eps_ 1) ≤ mul_SNo 2 t.
An exact proof term for the current goal is (nonneg_mul_SNo_Le 2 (eps_ 1) t H2S H0le2 HeS HtS Hepsle_t).
We prove the intermediate claim H1le2t: 1 ≤ mul_SNo 2 t.
rewrite the current goal using eps_1_half_eq2 (from right to left) at position 1.
An exact proof term for the current goal is H2eps_le_2t.
We prove the intermediate claim H0les: 0 ≤ add_SNo (mul_SNo 2 t) (minus_SNo 1).
We will prove 0 ≤ add_SNo (mul_SNo 2 t) (minus_SNo 1).
rewrite the current goal using (add_SNo_minus_SNo_rinv 1 SNo_1) (from right to left) at position 1.
An exact proof term for the current goal is (add_SNo_Le1 1 (minus_SNo 1) (mul_SNo 2 t) SNo_1 Hm1S (SNo_mul_SNo 2 t H2S HtS) H1le2t).
We prove the intermediate claim Hcases: 0 < add_SNo (mul_SNo 2 t) (minus_SNo 1) ∨ 0 = add_SNo (mul_SNo 2 t) (minus_SNo 1).
An exact proof term for the current goal is (SNoLeE 0 (add_SNo (mul_SNo 2 t) (minus_SNo 1)) SNo_0 HsS H0les).
Apply Hcases to the current goal.
Assume Hpos: 0 < add_SNo (mul_SNo 2 t) (minus_SNo 1).
We prove the intermediate claim H00: 0 < 0.
An exact proof term for the current goal is (SNoLt_tra 0 (add_SNo (mul_SNo 2 t) (minus_SNo 1)) 0 SNo_0 HsS SNo_0 Hpos Hslt0).
An exact proof term for the current goal is ((SNoLt_irref 0) H00).
Assume Heq: 0 = add_SNo (mul_SNo 2 t) (minus_SNo 1).
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 Hslt0.
An exact proof term for the current goal is ((SNoLt_irref 0) H00).
Assume Hlt: Rlt 1 (add_SNo (mul_SNo 2 t) (minus_SNo 1)).
We will prove False.
We prove the intermediate claim H1lts: 1 < add_SNo (mul_SNo 2 t) (minus_SNo 1).
An exact proof term for the current goal is (RltE_lt 1 (add_SNo (mul_SNo 2 t) (minus_SNo 1)) Hlt).
We prove the intermediate claim Hnlt_1t: ¬ (Rlt 1 t).
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 (andER (¬ (Rlt t 0)) (¬ (Rlt 1 t)) Hconj).
We prove the intermediate claim Htle1: t ≤ 1.
We will prove t ≤ 1.
Apply (SNoLtLe_or 1 t SNo_1 HtS) to the current goal.
Assume H1lt: 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 H1lt).
Apply FalseE to the current goal.
An exact proof term for the current goal is (Hnlt_1t Hrlt).
Assume Hle: t ≤ 1.
An exact proof term for the current goal is Hle.
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 H2t_le_2: mul_SNo 2 t ≤ mul_SNo 2 1.
An exact proof term for the current goal is (nonneg_mul_SNo_Le 2 t 1 H2S H0le2 HtS SNo_1 Htle1).
We prove the intermediate claim H2t_le_2': mul_SNo 2 t ≤ 2.
rewrite the current goal using (mul_SNo_oneR 2 SNo_2) (from right to left) at position 2.
An exact proof term for the current goal is H2t_le_2.
We prove the intermediate claim Hsle_2m1: add_SNo (mul_SNo 2 t) (minus_SNo 1) ≤ add_SNo 2 (minus_SNo 1).
An exact proof term for the current goal is (add_SNo_Le1 (mul_SNo 2 t) (minus_SNo 1) 2 (SNo_mul_SNo 2 t H2S HtS) Hm1S SNo_2 H2t_le_2').
We prove the intermediate claim H2m1eq1: add_SNo 2 (minus_SNo 1) = 1.
rewrite the current goal using add_SNo_1_1_2 (from right to left) at position 1.
rewrite the current goal using (add_SNo_assoc 1 1 (minus_SNo 1) SNo_1 SNo_1 Hm1S) (from right to left) at position 1.
rewrite the current goal using (add_SNo_minus_SNo_rinv 1 SNo_1) (from left to right) at position 1.
rewrite the current goal using (add_SNo_0R 1 SNo_1) (from left to right) at position 1.
Use reflexivity.
We prove the intermediate claim Hsle1: add_SNo (mul_SNo 2 t) (minus_SNo 1) ≤ 1.
We prove the intermediate claim H2m1S: SNo (add_SNo 2 (minus_SNo 1)).
An exact proof term for the current goal is (SNo_add_SNo 2 (minus_SNo 1) SNo_2 Hm1S).
We prove the intermediate claim H2m1le1: add_SNo 2 (minus_SNo 1) ≤ 1.
rewrite the current goal using H2m1eq1 (from left to right) at position 1.
An exact proof term for the current goal is (SNoLe_ref 1).
An exact proof term for the current goal is (SNoLe_tra (add_SNo (mul_SNo 2 t) (minus_SNo 1)) (add_SNo 2 (minus_SNo 1)) 1 HsS H2m1S SNo_1 Hsle_2m1 H2m1le1).
We prove the intermediate claim Hcases: add_SNo (mul_SNo 2 t) (minus_SNo 1) < 1 ∨ add_SNo (mul_SNo 2 t) (minus_SNo 1) = 1.
An exact proof term for the current goal is (SNoLeE (add_SNo (mul_SNo 2 t) (minus_SNo 1)) 1 HsS SNo_1 Hsle1).
Apply Hcases to the current goal.
Assume Hslt1: add_SNo (mul_SNo 2 t) (minus_SNo 1) < 1.
We prove the intermediate claim H11: 1 < 1.
An exact proof term for the current goal is (SNoLt_tra 1 (add_SNo (mul_SNo 2 t) (minus_SNo 1)) 1 SNo_1 HsS SNo_1 H1lts Hslt1).
An exact proof term for the current goal is ((SNoLt_irref 1) H11).
Assume Heq: add_SNo (mul_SNo 2 t) (minus_SNo 1) = 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 H1lts.
An exact proof term for the current goal is ((SNoLt_irref 1) H11).
∎