Let t be given.
Assume HtR: t ∈ R.
Assume Htne0: t ≠ 0.
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 HnumPos: 0 < num.
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 Ht0: t = 0.
Apply FalseE to the current goal.
An exact proof term for the current goal is (Htne0 Ht0).
Assume Hpos: 0 < mul_SNo t t.
An exact proof term for the current goal is Hpos.
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 HdivPos: 0 < div_SNo num den.
An exact proof term for the current goal is (div_SNo_pos_pos num den HnumS HdenS HnumPos HdenPos).
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 H0ltf: 0 < f.
rewrite the current goal using HfEq (from left to right).
An exact proof term for the current goal is HdivPos.
An exact proof term for the current goal is (RltI 0 f real_0 HfR H0ltf).
∎