We will prove mul_SNo two_thirds two_thirds < eps_ 1.
rewrite the current goal using two_thirds_eq_div_2_3 (from left to right) at position 1.
rewrite the current goal using two_thirds_eq_div_2_3 (from left to right) at position 1.
We prove the intermediate claim H3S: SNo 3.
An exact proof term for the current goal is (real_SNo 3 real_3).
rewrite the current goal using (mul_div_SNo_both 2 3 2 3 SNo_2 H3S SNo_2 H3S) (from left to right) at position 1.
rewrite the current goal using mul_SNo_2_2_eq_4 (from left to right) at position 1.
rewrite the current goal using mul_SNo_3_3_eq_9 (from left to right) at position 1.
rewrite the current goal using div_SNo_1_2_eq_eps_1 (from right to left).
We prove the intermediate claim H4S: SNo 4.
rewrite the current goal using mul_SNo_2_2_eq_4 (from right to left).
An exact proof term for the current goal is (SNo_mul_SNo 2 2 SNo_2 SNo_2).
We prove the intermediate claim H9S: SNo 9.
rewrite the current goal using mul_SNo_3_3_eq_9 (from right to left).
An exact proof term for the current goal is (SNo_mul_SNo 3 3 H3S H3S).
We prove the intermediate claim HdivS: SNo (div_SNo 1 2).
An exact proof term for the current goal is (SNo_div_SNo 1 2 SNo_1 SNo_2).
We prove the intermediate claim H8nat: nat_p 8.
We prove the intermediate claim H3nat: nat_p 3.
An exact proof term for the current goal is (nat_ordsucc 2 nat_2).
We prove the intermediate claim H4nat: nat_p 4.
An exact proof term for the current goal is (nat_ordsucc 3 H3nat).
We prove the intermediate claim H5nat: nat_p 5.
An exact proof term for the current goal is (nat_ordsucc 4 H4nat).
We prove the intermediate claim H6nat: nat_p 6.
An exact proof term for the current goal is (nat_ordsucc 5 H5nat).
We prove the intermediate claim H7nat: nat_p 7.
An exact proof term for the current goal is (nat_ordsucc 6 H6nat).
An exact proof term for the current goal is (nat_ordsucc 7 H7nat).
We prove the intermediate claim H9eq: 9 = ordsucc 8.
Use reflexivity.
We prove the intermediate claim H0in9: 0 ∈ 9.
rewrite the current goal using H9eq (from left to right).
An exact proof term for the current goal is (nat_0_in_ordsucc 8 H8nat).
We prove the intermediate claim Hord9: ordinal 9.
We prove the intermediate claim H9nat: nat_p 9.
An exact proof term for the current goal is (nat_ordsucc 8 H8nat).
An exact proof term for the current goal is (nat_p_ordinal 9 H9nat).
We prove the intermediate claim H0lt9: 0 < 9.
An exact proof term for the current goal is (ordinal_In_SNoLt 9 Hord9 0 H0in9).
Apply (div_SNo_pos_LtL 4 9 (div_SNo 1 2) H4S H9S HdivS H0lt9) to the current goal.
We will prove 4 < mul_SNo (div_SNo 1 2) 9.
We prove the intermediate claim HmulEq: mul_SNo (div_SNo 1 2) 9 = div_SNo (mul_SNo 1 9) 2.
An exact proof term for the current goal is (mul_div_SNo_R 1 2 9 SNo_1 SNo_2 H9S).
rewrite the current goal using HmulEq (from left to right).
rewrite the current goal using (mul_SNo_oneL 9 H9S) (from left to right) at position 1.
Apply (div_SNo_pos_LtR 9 2 4 H9S SNo_2 H4S SNoLt_0_2) to the current goal.
An exact proof term for the current goal is mul_SNo_4_2_lt_9.
∎