Let m be given.

Assume Hm.

Let n be given.

Assume Hn.

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

We will prove divides_nat n (n * m).

An exact proof term for the current goal is divides_nat_mul_SNo_R n Hn m Hm.

∎