Let a and t be given.
Assume HaR: a ∈ R.
Assume HtR: t ∈ R.
Assume HaPos: 0 < a.
Assume HaLt1: a < 1.
Set num to be the term mul_SNo t t.
Set den to be the term add_SNo (mul_SNo t t) (mul_SNo (add_SNo t (minus_SNo 1)) (add_SNo t (minus_SNo 1))).
We prove the intermediate claim HaS: SNo a.
An exact proof term for the current goal is (real_SNo a HaR).
We prove the intermediate claim HtS: SNo t.
An exact proof term for the current goal is (real_SNo t HtR).
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 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 HuS: SNo (add_SNo t (minus_SNo 1)).
An exact proof term for the current goal is (SNo_add_SNo t (minus_SNo 1) HtS Hm1S).
We prove the intermediate claim HsqS: SNo (mul_SNo (add_SNo t (minus_SNo 1)) (add_SNo t (minus_SNo 1))).
An exact proof term for the current goal is (SNo_mul_SNo (add_SNo t (minus_SNo 1)) (add_SNo t (minus_SNo 1)) HuS HuS).
We prove the intermediate claim HdenS: SNo den.
An exact proof term for the current goal is (SNo_add_SNo num (mul_SNo (add_SNo t (minus_SNo 1)) (add_SNo t (minus_SNo 1))) HnumS HsqS).
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 HfEq: apply_fun normalize01_fun t = 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.
Apply iffI to the current goal.
Assume Halt: a < apply_fun normalize01_fun t.
We prove the intermediate claim Halt': a < div_SNo num den.
rewrite the current goal using HfEq (from right to left) at position 1.
An exact proof term for the current goal is Halt.
An exact proof term for the current goal is (div_SNo_pos_LtR' num den a HnumS HdenS HaS HdenPos Halt').
Assume Hmul: mul_SNo a den < num.
We prove the intermediate claim Halt': a < div_SNo num den.
An exact proof term for the current goal is (div_SNo_pos_LtR num den a HnumS HdenS HaS HdenPos Hmul).
rewrite the current goal using HfEq (from left to right) at position 1.
An exact proof term for the current goal is Halt'.
∎