Let a and t be given.
Assume HaR: a ∈ R.
Assume HtR: t ∈ R.
We will prove (Rlt a (mul_SNo 2 t) ↔ Rlt (mul_SNo (eps_ 1) a) t).
Apply iffI to the current goal.
Assume Halt: Rlt a (mul_SNo 2 t).
We will prove Rlt (mul_SNo (eps_ 1) a) t.
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 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 Hm2tS: 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 HaltS: a < mul_SNo 2 t.
An exact proof term for the current goal is (RltE_lt a (mul_SNo 2 t) Halt).
We prove the intermediate claim Hmul: mul_SNo (eps_ 1) a < mul_SNo (eps_ 1) (mul_SNo 2 t).
An exact proof term for the current goal is (pos_mul_SNo_Lt (eps_ 1) a (mul_SNo 2 t) He1S H0lte1 HaS Hm2tS HaltS).
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': mul_SNo (eps_ 1) a < t.
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 Hmule1aR: mul_SNo (eps_ 1) a ∈ 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 HaReal: a ∈ real.
rewrite the current goal using HdefR (from right to left).
An exact proof term for the current goal is HaR.
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 a HaReal).
An exact proof term for the current goal is (RltI (mul_SNo (eps_ 1) a) t Hmule1aR HtR Hmul').
Assume Hlt: Rlt (mul_SNo (eps_ 1) a) t.
We will prove Rlt a (mul_SNo 2 t).
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 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 He1aS: SNo (mul_SNo (eps_ 1) a).
An exact proof term for the current goal is (SNo_mul_SNo (eps_ 1) a He1S HaS).
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: mul_SNo (eps_ 1) a < t.
An exact proof term for the current goal is (RltE_lt (mul_SNo (eps_ 1) a) t Hlt).
We prove the intermediate claim Hmul: mul_SNo 2 (mul_SNo (eps_ 1) a) < mul_SNo 2 t.
An exact proof term for the current goal is (pos_mul_SNo_Lt 2 (mul_SNo (eps_ 1) a) t H2S H0lt2 He1aS HtS HltS).
We prove the intermediate claim Heq: mul_SNo 2 (mul_SNo (eps_ 1) a) = a.
rewrite the current goal using (mul_SNo_assoc 2 (eps_ 1) a H2S He1S HaS) (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 a HaS).
We prove the intermediate claim Hmul': a < mul_SNo 2 t.
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 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 a (mul_SNo 2 t) HaR H2tR Hmul').
∎