Let m and n be given.

Assume Hm Hn Hmn.

Let k be given.

Assume Hk.

rewrite the current goal using mul_nat_com k Hk m Hm (from left to right).

rewrite the current goal using mul_nat_com k Hk n Hn (from left to right).

An exact proof term for the current goal is mul_nat_Subq_R m n Hm Hn Hmn k Hk.

∎