We prove the intermediate claim H2omega: 2 ∈ ω.

An exact proof term for the current goal is (nat_p_omega 2 nat_2).

rewrite the current goal using (add_SNo_1_ordsucc 2 H2omega) (from left to right).

rewrite the current goal using ordsucc_2_eq_3 (from left to right).

Use reflexivity.

∎