Let b and t be given.
Assume HbR: b ∈ R.
Assume HtR: t ∈ R.
Assume HbPos: 0 < b.
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 HbS: SNo b.
An exact proof term for the current goal is (real_SNo b HbR).
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 Hlt: apply_fun normalize01_fun t < b.
We prove the intermediate claim Hlt': div_SNo num den < b.
rewrite the current goal using HfEq (from right to left) at position 1.
An exact proof term for the current goal is Hlt.
An exact proof term for the current goal is (div_SNo_pos_LtL' num den b HnumS HdenS HbS HdenPos Hlt').
Assume Hmul: num < mul_SNo b den.
We prove the intermediate claim Hlt': div_SNo num den < b.
An exact proof term for the current goal is (div_SNo_pos_LtL num den b HnumS HdenS HbS HdenPos Hmul).
rewrite the current goal using HfEq (from left to right) at position 1.
An exact proof term for the current goal is Hlt'.
∎