We will prove mul_SNo 3 3 = 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 H3O: 3 ∈ ω.

An exact proof term for the current goal is (nat_p_omega 3 H3nat).

We prove the intermediate claim HmulEq: mul_nat 3 3 = mul_SNo 3 3.

An exact proof term for the current goal is (mul_nat_mul_SNo 3 H3O 3 H3O).

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

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

Use reflexivity.

∎