We will prove apply_fun normalize01_fun 0 = 0.
We prove the intermediate claim H0R: 0 ∈ R.
An exact proof term for the current goal is real_0.
We prove the intermediate claim Hdef: normalize01_fun = graph R (λt : set ⇒ 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))))).
Use reflexivity.
rewrite the current goal using Hdef (from left to right).
rewrite the current goal using (apply_fun_graph R (λt : set ⇒ 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))))) 0 H0R) (from left to right).
We prove the intermediate claim Hnum: mul_SNo 0 0 = 0.
An exact proof term for the current goal is (mul_SNo_zeroR 0 SNo_0).
rewrite the current goal using Hnum (from left to right) at position 1.
We prove the intermediate claim HdenS: SNo (add_SNo (mul_SNo 0 0) (mul_SNo (add_SNo 0 (minus_SNo 1)) (add_SNo 0 (minus_SNo 1)))).
We prove the intermediate claim H00S: SNo (mul_SNo 0 0).
An exact proof term for the current goal is (SNo_mul_SNo 0 0 SNo_0 SNo_0).
We prove the intermediate claim Hm1S: SNo (minus_SNo 1).
An exact proof term for the current goal is (SNo_minus_SNo 1 SNo_1).
We prove the intermediate claim H0m1S: SNo (add_SNo 0 (minus_SNo 1)).
An exact proof term for the current goal is (SNo_add_SNo 0 (minus_SNo 1) SNo_0 Hm1S).
We prove the intermediate claim HsqS: SNo (mul_SNo (add_SNo 0 (minus_SNo 1)) (add_SNo 0 (minus_SNo 1))).
An exact proof term for the current goal is (SNo_mul_SNo (add_SNo 0 (minus_SNo 1)) (add_SNo 0 (minus_SNo 1)) H0m1S H0m1S).
An exact proof term for the current goal is (SNo_add_SNo (mul_SNo 0 0) (mul_SNo (add_SNo 0 (minus_SNo 1)) (add_SNo 0 (minus_SNo 1))) H00S HsqS).
An exact proof term for the current goal is (div_SNo_0_num (add_SNo (mul_SNo 0 0) (mul_SNo (add_SNo 0 (minus_SNo 1)) (add_SNo 0 (minus_SNo 1)))) HdenS).
∎