Theorem: Misc.Nat.zero_dvd_iff (LeanSAT/Util/Misc.lean)

State before:
a : Nat
h : a = 0
⊢ 0 ∣ a
Tactic:
rw [h]
State after:
a : Nat
h : a = 0
⊢ 0 ∣ 0

State before:
a : Nat
h : a = 0
⊢ 0 ∣ 0
Tactic:
exact ⟨0, by simp⟩
State after:
no goals

State before:
a : Nat
h : a = 0
⊢ 0 = 0 * 0
Tactic:
simp
State after:
no goals