no goals
R : Type ?u.25956
S : Type ?u.25959
M : Type u_1
inst✝² : MonoidWithZero M
inst✝¹ : NoZeroDivisors M
inst✝ : Nontrivial M
a : M
n : ℕ
⊢ a ^ n = 0 ↔ a = 0 ∧ n ≠ 0
cases (zero_le n).eq_or_gt <;> simp [*, ne_of_gt]