∀a,b:ℤ.  ((a | b) 
⇒ (∀n:ℤ. ((n * a) | (n * b))))
{ Auto }
1. a : ℤ
2. b : ℤ
3. a | b
4. n : ℤ
⊢ (n * a) | (n * b)