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

State before:
a : Nat
h : 0 ∣ a
⊢ a = 0
Tactic:
rw [Nat.dvd_iff_mod_eq_zero] at h
State after:
a : Nat
h : a % 0 = 0
⊢ a = 0

State before:
a : Nat
h : a % 0 = 0
⊢ a = 0
Tactic:
simp only [Nat.mod_zero] at h
State after:
a : Nat
h : a = 0
⊢ a = 0

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