Let t be given.
Assume HtR: t ∈ R.
Assume Htne1: t ≠ 1.
Set f to be the term apply_fun normalize01_fun t.
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 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).
We prove the intermediate claim HuS: SNo u.
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 HdenPos: 0 < den.
An exact proof term for the current goal is (normalize01_fun_den_pos t HtR).
We prove the intermediate claim HuNe0: u ≠ 0.
Assume Hu0: u = 0.
We prove the intermediate claim Ht1: t = 1.
We prove the intermediate claim HtEq: add_SNo u 1 = t.
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).
An exact proof term for the current goal is (Htne1 Ht1).
We prove the intermediate claim Hu2Pos: 0 < u2.
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 Hu0: u = 0.
Apply FalseE to the current goal.
An exact proof term for the current goal is (HuNe0 Hu0).
Assume Hpos: 0 < mul_SNo u u.
An exact proof term for the current goal is Hpos.
We prove the intermediate claim HnumLtDen: num < den.
We prove the intermediate claim Hnum0: add_SNo num 0 = num.
An exact proof term for the current goal is (add_SNo_0R num HnumS).
rewrite the current goal using Hnum0 (from right to left) at position 1.
An exact proof term for the current goal is (add_SNo_Lt2 num 0 u2 HnumS SNo_0 Hu2S Hu2Pos).
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).
Use reflexivity.
We prove the intermediate claim HdivLt1: div_SNo num den < 1.
We prove the intermediate claim HnumLt1den: num < mul_SNo 1 den.
rewrite the current goal using (mul_SNo_oneL den HdenS) (from left to right).
An exact proof term for the current goal is HnumLtDen.
An exact proof term for the current goal is (div_SNo_pos_LtL num den 1 HnumS HdenS SNo_1 HdenPos HnumLt1den).
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 HfLt1: f < 1.
rewrite the current goal using HfEq (from left to right).
An exact proof term for the current goal is HdivLt1.
An exact proof term for the current goal is (RltI f 1 HfR real_1 HfLt1).
∎