Let t and b be given.
Assume HtR: t ∈ R.
Assume HbR: b ∈ R.
We will prove (Rlt (mul_SNo 2 t) b ↔ Rlt t (mul_SNo (eps_ 1) b)).
Apply iffI to the current goal.
Assume Hlt: Rlt (mul_SNo 2 t) b.
We will prove Rlt t (mul_SNo (eps_ 1) b).
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 HbS: SNo b.
An exact proof term for the current goal is (real_SNo b HbR).
We prove the intermediate claim H2S: SNo 2.
An exact proof term for the current goal is SNo_2.
We prove the intermediate claim He1S: SNo (eps_ 1).
An exact proof term for the current goal is SNo_eps_1.
We prove the intermediate claim H2tS: SNo (mul_SNo 2 t).
An exact proof term for the current goal is (SNo_mul_SNo 2 t H2S HtS).
We prove the intermediate claim H0lte1: 0 < (eps_ 1).
An exact proof term for the current goal is (RltE_lt 0 (eps_ 1) eps_1_pos_R).
We prove the intermediate claim HltS: mul_SNo 2 t < b.
An exact proof term for the current goal is (RltE_lt (mul_SNo 2 t) b Hlt).
We prove the intermediate claim Hmul: mul_SNo (eps_ 1) (mul_SNo 2 t) < mul_SNo (eps_ 1) b.
An exact proof term for the current goal is (pos_mul_SNo_Lt (eps_ 1) (mul_SNo 2 t) b He1S H0lte1 H2tS HbS HltS).
We prove the intermediate claim Heq: mul_SNo (eps_ 1) (mul_SNo 2 t) = t.
rewrite the current goal using (mul_SNo_assoc (eps_ 1) 2 t He1S H2S HtS) (from left to right).
rewrite the current goal using (mul_SNo_com (eps_ 1) 2 He1S H2S) (from left to right).
rewrite the current goal using eps_1_half_eq2 (from left to right).
An exact proof term for the current goal is (mul_SNo_oneL t HtS).
We prove the intermediate claim Hmul': t < mul_SNo (eps_ 1) b.
rewrite the current goal using Heq (from right to left) at position 1.
An exact proof term for the current goal is Hmul.
We prove the intermediate claim He1bR: mul_SNo (eps_ 1) b ∈ R.
We prove the intermediate claim HdefR: R = real.
Use reflexivity.
rewrite the current goal using HdefR (from left to right).
We prove the intermediate claim HbReal: b ∈ real.
rewrite the current goal using HdefR (from right to left).
An exact proof term for the current goal is HbR.
We prove the intermediate claim He1Real: (eps_ 1) ∈ real.
rewrite the current goal using HdefR (from right to left).
An exact proof term for the current goal is eps_1_in_R.
An exact proof term for the current goal is (real_mul_SNo (eps_ 1) He1Real b HbReal).
An exact proof term for the current goal is (RltI t (mul_SNo (eps_ 1) b) HtR He1bR Hmul').
Assume Hlt: Rlt t (mul_SNo (eps_ 1) b).
We will prove Rlt (mul_SNo 2 t) b.
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 HbS: SNo b.
An exact proof term for the current goal is (real_SNo b HbR).
We prove the intermediate claim H2S: SNo 2.
An exact proof term for the current goal is SNo_2.
We prove the intermediate claim He1S: SNo (eps_ 1).
An exact proof term for the current goal is SNo_eps_1.
We prove the intermediate claim He1bS: SNo (mul_SNo (eps_ 1) b).
An exact proof term for the current goal is (SNo_mul_SNo (eps_ 1) b He1S HbS).
We prove the intermediate claim H0lt2: 0 < 2.
An exact proof term for the current goal is (SNoLt_0_2).
We prove the intermediate claim HltS: t < mul_SNo (eps_ 1) b.
An exact proof term for the current goal is (RltE_lt t (mul_SNo (eps_ 1) b) Hlt).
We prove the intermediate claim Hmul: mul_SNo 2 t < mul_SNo 2 (mul_SNo (eps_ 1) b).
An exact proof term for the current goal is (pos_mul_SNo_Lt 2 t (mul_SNo (eps_ 1) b) H2S H0lt2 HtS He1bS HltS).
We prove the intermediate claim Heq: mul_SNo 2 (mul_SNo (eps_ 1) b) = b.
rewrite the current goal using (mul_SNo_assoc 2 (eps_ 1) b H2S He1S HbS) (from left to right).
rewrite the current goal using eps_1_half_eq2 (from left to right).
An exact proof term for the current goal is (mul_SNo_oneL b HbS).
We prove the intermediate claim Hmul': mul_SNo 2 t < b.
rewrite the current goal using Heq (from right to left).
An exact proof term for the current goal is Hmul.
We prove the intermediate claim H2tR: mul_SNo 2 t ∈ R.
We prove the intermediate claim HdefR: R = real.
Use reflexivity.
rewrite the current goal using HdefR (from left to right).
We prove the intermediate claim H2Real: 2 ∈ real.
rewrite the current goal using HdefR (from right to left).
An exact proof term for the current goal is real_2.
We prove the intermediate claim HtReal: t ∈ real.
rewrite the current goal using HdefR (from right to left).
An exact proof term for the current goal is HtR.
An exact proof term for the current goal is (real_mul_SNo 2 H2Real t HtReal).
An exact proof term for the current goal is (RltI (mul_SNo 2 t) b H2tR HbR Hmul').
∎