We will prove mul_SNo 2 2 = 4.

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 HmulEq: mul_nat 2 2 = mul_SNo 2 2.

An exact proof term for the current goal is (mul_nat_mul_SNo 2 H2O 2 H2O).

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

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

Use reflexivity.

∎