Let m be given.

Assume Hm.

Let n be given.

Assume Hn.

rewrite the current goal using mul_nat_com m (omega_nat_p m Hm) n (omega_nat_p 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_mulR n Hn m Hm.

∎