Theorem: Nat.not_dvd_of_mod_neq_zero (ListPowersProblem.lean)

State before:
a b : ℕ
⊢ a % b ≠ 0 → ¬b ∣ a
Tactic:
rw [Nat.dvd_iff_mod_eq_zero]
State after:
a b : ℕ
⊢ a % b ≠ 0 → ¬a % b = 0

State before:
a b : ℕ
⊢ a % b ≠ 0 → ¬a % b = 0
Tactic:
exact id
State after:
no goals