α : Type u_1
inst✝¹ : Monoid α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a b : α
⊢ (∀ (n : ℕ), a ^ (n + 1) ∣ b) ↔ ∀ (n : ℕ), a ^ n ∣ b
α : Type u_1
inst✝¹ : Monoid α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a b : α
⊢ (∀ (n : ℕ), ¬¬a ^ (n + 1) ∣ b) ↔ ∀ (n : ℕ), a ^ n ∣ b
simp only [Classical.not_not]
no goals
α : Type u_1
inst✝¹ : Monoid α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a b : α
⊢ (∀ (n : ℕ), a ^ (n + 1) ∣ b) ↔ ∀ (n : ℕ), a ^ n ∣ b
exact
  ⟨fun h n =>
    Nat.casesOn n
      (by
        rw [_root_.pow_zero]
        exact one_dvd _)
      fun n => h _,
    fun h n => h _⟩
α : Type u_1
inst✝¹ : Monoid α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a b : α
h : ∀ (n : ℕ), a ^ (n + 1) ∣ b
n : ℕ
⊢ 1 ∣ b
α : Type u_1
inst✝¹ : Monoid α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a b : α
h : ∀ (n : ℕ), a ^ (n + 1) ∣ b
n : ℕ
⊢ a ^ zero ∣ b
rw [_root_.pow_zero]
no goals
α : Type u_1
inst✝¹ : Monoid α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a b : α
h : ∀ (n : ℕ), a ^ (n + 1) ∣ b
n : ℕ
⊢ 1 ∣ b
exact one_dvd _