no goals
M : Type ?u.2595779
N : Type ?u.2595782
G : Type ?u.2595785
R : Type ?u.2595788
S : Type ?u.2595791
F : Type ?u.2595794
inst✝⁴ : CommMonoid M
inst✝³ : CommMonoid N
inst✝² : DivisionCommMonoid G
k l✝ : ℕ
M₀ : Type u_1
inst✝¹ : CommMonoidWithZero M₀
inst✝ : Nontrivial M₀
l : ℕ
hl : 0 ^ l = 1
⊢ 0 ∣ l
simpa [zero_pow_eq, show ∀ p, ¬p → False ↔ p from @Classical.not_not] using hl