Let m, n and k be given.

Assume Hk: k ∈ int.

Assume H1: divides_int m n.

Apply H1 to the current goal.

Assume H.

Apply H to the current goal.

Assume Hm: m ∈ int.

Assume Hn: n ∈ int.

Assume _.

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

We will prove divides_int m (n * k).

An exact proof term for the current goal is divides_int_mul_SNo_L m n k Hk H1.

∎