Let t be given.
Assume HtI: t ∈ unit_interval.
We will prove apply_fun flip_unit_interval t ∈ unit_interval.
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 Htprop: ¬ (Rlt t 0) ∧ ¬ (Rlt 1 t).
An exact proof term for the current goal is (SepE2 R (λx0 : set ⇒ ¬ (Rlt x0 0) ∧ ¬ (Rlt 1 x0)) t HtI).
We prove the intermediate claim Hnlt_t0: ¬ (Rlt t 0).
An exact proof term for the current goal is (andEL (¬ (Rlt t 0)) (¬ (Rlt 1 t)) Htprop).
We prove the intermediate claim Hnlt_1t: ¬ (Rlt 1 t).
An exact proof term for the current goal is (andER (¬ (Rlt t 0)) (¬ (Rlt 1 t)) Htprop).
We prove the intermediate claim HmR: minus_SNo t ∈ R.
An exact proof term for the current goal is (real_minus_SNo t HtR).
rewrite the current goal using (flip_unit_interval_apply t HtI) (from left to right).
We will prove (add_SNo 1 (minus_SNo t)) ∈ unit_interval.
We prove the intermediate claim HsumR: add_SNo 1 (minus_SNo t) ∈ R.
An exact proof term for the current goal is (real_add_SNo 1 real_1 (minus_SNo t) HmR).
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 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 HmtS: SNo (minus_SNo t).
An exact proof term for the current goal is (real_SNo (minus_SNo t) HmR).
We prove the intermediate claim Hnlt_sum0: ¬ (Rlt (add_SNo 1 (minus_SNo t)) 0).
Assume Hlt: Rlt (add_SNo 1 (minus_SNo t)) 0.
We will prove False.
We prove the intermediate claim HltS: (add_SNo 1 (minus_SNo t)) < 0.
An exact proof term for the current goal is (RltE_lt (add_SNo 1 (minus_SNo t)) 0 Hlt).
We prove the intermediate claim HltS1: (add_SNo 1 (minus_SNo t)) < (add_SNo 1 (minus_SNo 1)).
rewrite the current goal using (add_SNo_minus_SNo_rinv 1 SNo_1) (from left to right).
An exact proof term for the current goal is HltS.
We prove the intermediate claim Hmtltm1: (minus_SNo t) < (minus_SNo 1).
An exact proof term for the current goal is (add_SNo_Lt2_cancel 1 (minus_SNo t) (minus_SNo 1) SNo_1 HmtS Hm1S HltS1).
We prove the intermediate claim H1ltmm: 1 < minus_SNo (minus_SNo t).
An exact proof term for the current goal is (minus_SNo_Lt_contra2 (minus_SNo t) 1 HmtS SNo_1 Hmtltm1).
We prove the intermediate claim H1ltt: 1 < t.
rewrite the current goal using (minus_SNo_invol t HtS) (from right to left).
An exact proof term for the current goal is H1ltmm.
We prove the intermediate claim H1lt: Rlt 1 t.
An exact proof term for the current goal is (RltI 1 t real_1 HtR H1ltt).
An exact proof term for the current goal is (Hnlt_1t H1lt).
We prove the intermediate claim Hnlt_1sum: ¬ (Rlt 1 (add_SNo 1 (minus_SNo t))).
Assume Hlt: Rlt 1 (add_SNo 1 (minus_SNo t)).
We will prove False.
We prove the intermediate claim HltS: 1 < (add_SNo 1 (minus_SNo t)).
An exact proof term for the current goal is (RltE_lt 1 (add_SNo 1 (minus_SNo t)) Hlt).
We prove the intermediate claim HltS1: (add_SNo 1 0) < (add_SNo 1 (minus_SNo t)).
rewrite the current goal using (add_SNo_0R 1 SNo_1) (from left to right).
An exact proof term for the current goal is HltS.
We prove the intermediate claim H0ltmt: 0 < (minus_SNo t).
An exact proof term for the current goal is (add_SNo_Lt2_cancel 1 0 (minus_SNo t) SNo_1 SNo_0 HmtS HltS1).
We prove the intermediate claim Htltm0: t < minus_SNo 0.
An exact proof term for the current goal is (minus_SNo_Lt_contra2 0 t SNo_0 HtS H0ltmt).
We prove the intermediate claim Htlt0S: t < 0.
rewrite the current goal using minus_SNo_0 (from right to left).
An exact proof term for the current goal is Htltm0.
We prove the intermediate claim Htlt0: Rlt t 0.
An exact proof term for the current goal is (RltI t 0 HtR real_0 Htlt0S).
An exact proof term for the current goal is (Hnlt_t0 Htlt0).
An exact proof term for the current goal is (SepI R (λx0 : set ⇒ ¬ (Rlt x0 0) ∧ ¬ (Rlt 1 x0)) (add_SNo 1 (minus_SNo t)) HsumR (andI (¬ (Rlt (add_SNo 1 (minus_SNo t)) 0)) (¬ (Rlt 1 (add_SNo 1 (minus_SNo t)))) Hnlt_sum0 Hnlt_1sum)).
∎