We will prove apply_fun normalize01_fun 1 = 1.
We prove the intermediate claim H1R: 1 ∈ R.
An exact proof term for the current goal is real_1.
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))))) 1 H1R) (from left to right).
rewrite the current goal using (mul_SNo_oneR 1 SNo_1) (from left to right).
rewrite the current goal using (add_SNo_minus_SNo_rinv 1 SNo_1) (from left to right).
rewrite the current goal using (mul_SNo_zeroR 0 SNo_0) (from left to right).
rewrite the current goal using (add_SNo_0R 1 SNo_1) (from left to right).
We prove the intermediate claim Hrecip1: recip_SNo 1 = 1.
We prove the intermediate claim H1neq0: 1 ≠ 0.
An exact proof term for the current goal is neq_1_0.
We prove the intermediate claim Hinv: mul_SNo 1 (recip_SNo 1) = 1.
An exact proof term for the current goal is (recip_SNo_invR 1 SNo_1 H1neq0).
rewrite the current goal using (mul_SNo_oneL (recip_SNo 1) (SNo_recip_SNo 1 SNo_1)) (from right to left) at position 1.
An exact proof term for the current goal is Hinv.
We prove the intermediate claim Hdivdef: div_SNo 1 1 = mul_SNo 1 (recip_SNo 1).
Use reflexivity.
rewrite the current goal using Hdivdef (from left to right).
rewrite the current goal using Hrecip1 (from left to right).
rewrite the current goal using (mul_SNo_oneR 1 SNo_1) (from left to right).
Use reflexivity.
∎