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