Let n be given.

Assume Hn.

Let m be given.

Assume Hm.

rewrite the current goal using mul_nat_mul_SNo n Hn m Hm (from right to left).

Apply nat_p_omega to the current goal.

An exact proof term for the current goal is mul_nat_p n (omega_nat_p n Hn) m (omega_nat_p m Hm).

∎