Let t be given.
Assume HtR: t ∈ R.
We will prove apply_fun normalize01_fun t ∈ R.
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 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 HnumR: mul_SNo t t ∈ R.
An exact proof term for the current goal is (real_mul_SNo t HtR t HtR).
We prove the intermediate claim Htminus1R: add_SNo t (minus_SNo 1) ∈ R.
An exact proof term for the current goal is (real_add_SNo t HtR (minus_SNo 1) Hm1R).
We prove the intermediate claim Hsq2R: mul_SNo (add_SNo t (minus_SNo 1)) (add_SNo t (minus_SNo 1)) ∈ R.
An exact proof term for the current goal is (real_mul_SNo (add_SNo t (minus_SNo 1)) Htminus1R (add_SNo t (minus_SNo 1)) Htminus1R).
We prove the intermediate claim HdenR: add_SNo (mul_SNo t t) (mul_SNo (add_SNo t (minus_SNo 1)) (add_SNo t (minus_SNo 1))) ∈ R.
An exact proof term for the current goal is (real_add_SNo (mul_SNo t t) HnumR (mul_SNo (add_SNo t (minus_SNo 1)) (add_SNo t (minus_SNo 1))) Hsq2R).
An exact proof term for the current goal is (real_div_SNo (mul_SNo t t) HnumR (add_SNo (mul_SNo t t) (mul_SNo (add_SNo t (minus_SNo 1)) (add_SNo t (minus_SNo 1)))) HdenR).
∎