We will prove mul_SNo 4 2 < 9.
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).
We prove the intermediate claim H8nat: nat_p 8.
An exact proof term for the current goal is (nat_ordsucc 7 H7nat).
We prove the intermediate claim H9nat: nat_p 9.
An exact proof term for the current goal is (nat_ordsucc 8 H8nat).
We prove the intermediate claim H4O: 4 ∈ ω.
An exact proof term for the current goal is (nat_p_omega 4 H4nat).
We prove the intermediate claim H2O: 2 ∈ ω.
An exact proof term for the current goal is (nat_p_omega 2 nat_2).
We prove the intermediate claim HmulNatEq: mul_nat 4 2 = mul_SNo 4 2.
An exact proof term for the current goal is (mul_nat_mul_SNo 4 H4O 2 H2O).
rewrite the current goal using HmulNatEq (from right to left) at position 1.
rewrite the current goal using mul_nat_4_2_eq_8 (from left to right).
We prove the intermediate claim Hord9: ordinal 9.
An exact proof term for the current goal is (nat_p_ordinal 9 H9nat).
We prove the intermediate claim H9eq: ordsucc 8 = 9.
Use reflexivity.
We prove the intermediate claim H8in9: 8 ∈ 9.
rewrite the current goal using H9eq (from right to left).
An exact proof term for the current goal is (ordsuccI2 8).
An exact proof term for the current goal is (ordinal_In_SNoLt 9 Hord9 8 H8in9).
∎