case mp
R : Type ?u.47966
S : Type ?u.47969
M : Type u_1
inst✝¹ : MonoidWithZero M
inst✝ : Nontrivial M
n : ℕ
h : 0 ^ n = 0
⊢ 0 < n

case mpr
R : Type ?u.47966
S : Type ?u.47969
M : Type u_1
inst✝¹ : MonoidWithZero M
inst✝ : Nontrivial M
n : ℕ
h : 0 < n
⊢ 0 ^ n = 0
R : Type ?u.47966
S : Type ?u.47969
M : Type u_1
inst✝¹ : MonoidWithZero M
inst✝ : Nontrivial M
n : ℕ
⊢ 0 ^ n = 0 ↔ 0 < n
constructor <;> intro h
case mp
R : Type ?u.47966
S : Type ?u.47969
M : Type u_1
inst✝¹ : MonoidWithZero M
inst✝ : Nontrivial M
n : ℕ
h : 0 ^ n = 0
⊢ n ≠ 0
case mp
R : Type ?u.47966
S : Type ?u.47969
M : Type u_1
inst✝¹ : MonoidWithZero M
inst✝ : Nontrivial M
n : ℕ
h : 0 ^ n = 0
⊢ 0 < n
rw [pos_iff_ne_zero]
case mp
R : Type ?u.47966
S : Type ?u.47969
M : Type u_1
inst✝¹ : MonoidWithZero M
inst✝ : Nontrivial M
h : 0 ^ 0 = 0
⊢ False
case mp
R : Type ?u.47966
S : Type ?u.47969
M : Type u_1
inst✝¹ : MonoidWithZero M
inst✝ : Nontrivial M
n : ℕ
h : 0 ^ n = 0
⊢ n ≠ 0
rintro rfl
no goals
case mp
R : Type ?u.47966
S : Type ?u.47969
M : Type u_1
inst✝¹ : MonoidWithZero M
inst✝ : Nontrivial M
h : 0 ^ 0 = 0
⊢ False
simp at h
no goals
case mpr
R : Type ?u.47966
S : Type ?u.47969
M : Type u_1
inst✝¹ : MonoidWithZero M
inst✝ : Nontrivial M
n : ℕ
h : 0 < n
⊢ 0 ^ n = 0
exact zero_pow' n h.ne.symm