Let t be given.
Assume HtR: t ∈ R.
We will prove apply_fun normalize01_fun t ∈ unit_interval.
Set f to be the term apply_fun normalize01_fun t.
We prove the intermediate claim HfR: f ∈ R.
An exact proof term for the current goal is (normalize01_fun_value_in_R t HtR).
We prove the intermediate claim HtS: SNo t.
An exact proof term for the current goal is (real_SNo t HtR).
Set num to be the term mul_SNo t t.
Set u to be the term add_SNo t (minus_SNo 1).
Set u2 to be the term mul_SNo u u.
Set den to be the term add_SNo num u2.
We prove the intermediate claim HnumS: SNo num.
An exact proof term for the current goal is (SNo_mul_SNo t t HtS HtS).
We prove the intermediate claim HuS: SNo u.
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 HuR: u ∈ R.
An exact proof term for the current goal is (real_add_SNo t HtR (minus_SNo 1) Hm1R).
An exact proof term for the current goal is (real_SNo u HuR).
We prove the intermediate claim Hu2S: SNo u2.
An exact proof term for the current goal is (SNo_mul_SNo u u HuS HuS).
We prove the intermediate claim HdenS: SNo den.
An exact proof term for the current goal is (SNo_add_SNo num u2 HnumS Hu2S).
We prove the intermediate claim HfEq: f = div_SNo num den.
We prove the intermediate claim Hdef: normalize01_fun = graph R (λt0 : set ⇒ div_SNo (mul_SNo t0 t0) (add_SNo (mul_SNo t0 t0) (mul_SNo (add_SNo t0 (minus_SNo 1)) (add_SNo t0 (minus_SNo 1))))).
Use reflexivity.
rewrite the current goal using Hdef (from left to right).
rewrite the current goal using (apply_fun_graph R (λt0 : set ⇒ div_SNo (mul_SNo t0 t0) (add_SNo (mul_SNo t0 t0) (mul_SNo (add_SNo t0 (minus_SNo 1)) (add_SNo t0 (minus_SNo 1))))) t HtR) (from left to right).
We will prove div_SNo (mul_SNo t t) (add_SNo (mul_SNo t t) (mul_SNo (add_SNo t (minus_SNo 1)) (add_SNo t (minus_SNo 1)))) = div_SNo num den.
Use reflexivity.
We prove the intermediate claim H0le_num: 0 ≤ num.
An exact proof term for the current goal is (SNo_sqr_nonneg t HtS).
We prove the intermediate claim H0le_u2: 0 ≤ u2.
An exact proof term for the current goal is (SNo_sqr_nonneg u HuS).
We prove the intermediate claim H0le_den: 0 ≤ den.
We prove the intermediate claim H00le: add_SNo 0 0 ≤ add_SNo num u2.
An exact proof term for the current goal is (add_SNo_Le3 0 0 num u2 SNo_0 SNo_0 HnumS Hu2S H0le_num H0le_u2).
We prove the intermediate claim HdenDef: den = add_SNo num u2.
Use reflexivity.
rewrite the current goal using HdenDef (from left to right) at position 1.
rewrite the current goal using (add_SNo_0R 0 SNo_0) (from right to left) at position 1.
An exact proof term for the current goal is H00le.
We prove the intermediate claim Hden_ne0: den ≠ 0.
Assume Hden0: den = 0.
We will prove False.
We prove the intermediate claim Hnum_le_den: num ≤ den.
An exact proof term for the current goal is (SNoLe_add_nonneg_right num u2 HnumS Hu2S H0le_u2).
We prove the intermediate claim Hu2_le_den: u2 ≤ den.
We prove the intermediate claim HdenDef: den = add_SNo num u2.
Use reflexivity.
rewrite the current goal using HdenDef (from left to right) at position 1.
rewrite the current goal using (add_SNo_com num u2 HnumS Hu2S) (from left to right) at position 1.
An exact proof term for the current goal is (SNoLe_add_nonneg_right u2 num Hu2S HnumS H0le_num).
We prove the intermediate claim Hdenle0: den ≤ 0.
rewrite the current goal using Hden0 (from left to right) at position 1.
An exact proof term for the current goal is (SNoLe_ref 0).
We prove the intermediate claim Hnumle0: num ≤ 0.
An exact proof term for the current goal is (SNoLe_tra num den 0 HnumS HdenS SNo_0 Hnum_le_den Hdenle0).
We prove the intermediate claim Hu2le0: u2 ≤ 0.
An exact proof term for the current goal is (SNoLe_tra u2 den 0 Hu2S HdenS SNo_0 Hu2_le_den Hdenle0).
We prove the intermediate claim Hnum0: num = 0.
An exact proof term for the current goal is (SNoLe_antisym num 0 HnumS SNo_0 Hnumle0 H0le_num).
We prove the intermediate claim Hu20: u2 = 0.
An exact proof term for the current goal is (SNoLe_antisym u2 0 Hu2S SNo_0 Hu2le0 H0le_u2).
We prove the intermediate claim Ht0: t = 0.
We prove the intermediate claim Hcases: t = 0 ∨ 0 < mul_SNo t t.
An exact proof term for the current goal is (SNo_zero_or_sqr_pos t HtS).
Apply Hcases to the current goal.
Assume H0: t = 0.
An exact proof term for the current goal is H0.
Assume Hpos: 0 < mul_SNo t t.
We prove the intermediate claim Hpos0: 0 < 0.
rewrite the current goal using Hnum0 (from right to left) at position 2.
An exact proof term for the current goal is Hpos.
An exact proof term for the current goal is (FalseE ((SNoLt_irref 0) Hpos0) (t = 0)).
We prove the intermediate claim Hu0: u = 0.
We prove the intermediate claim Hcases: u = 0 ∨ 0 < mul_SNo u u.
An exact proof term for the current goal is (SNo_zero_or_sqr_pos u HuS).
Apply Hcases to the current goal.
Assume H0: u = 0.
An exact proof term for the current goal is H0.
Assume Hpos: 0 < mul_SNo u u.
We prove the intermediate claim Hpos0: 0 < 0.
rewrite the current goal using Hu20 (from right to left) at position 2.
An exact proof term for the current goal is Hpos.
An exact proof term for the current goal is (FalseE ((SNoLt_irref 0) Hpos0) (u = 0)).
We prove the intermediate claim Ht1: t = 1.
We prove the intermediate claim HuDef: u = add_SNo t (minus_SNo 1).
Use reflexivity.
We prove the intermediate claim HtEq: add_SNo u 1 = t.
rewrite the current goal using HuDef (from left to right).
An exact proof term for the current goal is (add_SNo_minus_R2' t 1 HtS SNo_1).
rewrite the current goal using HtEq (from right to left).
rewrite the current goal using Hu0 (from left to right).
An exact proof term for the current goal is (add_SNo_0L 1 SNo_1).
We prove the intermediate claim H01: 0 = 1.
rewrite the current goal using Ht0 (from right to left) at position 1.
An exact proof term for the current goal is Ht1.
An exact proof term for the current goal is (neq_0_1 H01).
We prove the intermediate claim Hden_pos: 0 < den.
We prove the intermediate claim Hcases: 0 < den ∨ 0 = den.
An exact proof term for the current goal is (SNoLeE 0 den SNo_0 HdenS H0le_den).
Apply Hcases to the current goal.
Assume Hpos: 0 < den.
An exact proof term for the current goal is Hpos.
Assume Heq: 0 = den.
Apply FalseE to the current goal.
We prove the intermediate claim Hden0: den = 0.
rewrite the current goal using Heq (from right to left).
Use reflexivity.
An exact proof term for the current goal is (Hden_ne0 Hden0).
We prove the intermediate claim Hden_ne0': den ≠ 0.
An exact proof term for the current goal is Hden_ne0.
Apply (SepI R (λx0 : set ⇒ ¬ (Rlt x0 0) ∧ ¬ (Rlt 1 x0)) f HfR) to the current goal.
Apply andI to the current goal.
Assume Hlt: Rlt f 0.
We will prove False.
We prove the intermediate claim HfS: SNo f.
An exact proof term for the current goal is (real_SNo f HfR).
We prove the intermediate claim HfLt0: f < 0.
An exact proof term for the current goal is (RltE_lt f 0 Hlt).
We prove the intermediate claim HdenLt0: 0 < den.
An exact proof term for the current goal is Hden_pos.
We prove the intermediate claim HmulLt0: mul_SNo f den < 0.
An exact proof term for the current goal is (mul_SNo_neg_pos f den HfS HdenS HfLt0 HdenLt0).
We prove the intermediate claim HmulEq: mul_SNo f den = num.
rewrite the current goal using HfEq (from left to right).
An exact proof term for the current goal is (mul_div_SNo_invL num den HnumS HdenS Hden_ne0').
We prove the intermediate claim HnumLt0: num < 0.
rewrite the current goal using HmulEq (from right to left) at position 1.
An exact proof term for the current goal is HmulLt0.
We prove the intermediate claim Hbad: 0 < 0.
An exact proof term for the current goal is (SNoLeLt_tra 0 num 0 SNo_0 HnumS SNo_0 H0le_num HnumLt0).
An exact proof term for the current goal is (FalseE ((SNoLt_irref 0) Hbad) False).
Assume Hlt: Rlt 1 f.
We will prove False.
We prove the intermediate claim H1Lt: 1 < f.
An exact proof term for the current goal is (RltE_lt 1 f Hlt).
We prove the intermediate claim HdenLt0: 0 < den.
An exact proof term for the current goal is Hden_pos.
We prove the intermediate claim HfDiv: f = div_SNo num den.
An exact proof term for the current goal is HfEq.
We prove the intermediate claim H1LtDiv: 1 < div_SNo num den.
rewrite the current goal using HfDiv (from right to left).
An exact proof term for the current goal is H1Lt.
We prove the intermediate claim HdenLtNum: den < num.
We prove the intermediate claim H1denLt: mul_SNo 1 den < num.
An exact proof term for the current goal is (div_SNo_pos_LtR' num den 1 HnumS HdenS SNo_1 HdenLt0 H1LtDiv).
rewrite the current goal using (mul_SNo_oneL den HdenS) (from right to left) at position 1.
An exact proof term for the current goal is H1denLt.
We prove the intermediate claim HnumLeDen: num ≤ den.
An exact proof term for the current goal is (SNoLe_add_nonneg_right num u2 HnumS Hu2S H0le_u2).
We prove the intermediate claim Hbad: den < den.
An exact proof term for the current goal is (SNoLtLe_tra den num den HdenS HnumS HdenS HdenLtNum HnumLeDen).
An exact proof term for the current goal is (FalseE ((SNoLt_irref den) Hbad) False).
∎