case intro
a b n : ℕ
hn : 0 < succ n
⊢ coprime (a ^ succ n) b ↔ coprime a b
n : ℕ
hn : 0 < n
a b : ℕ
⊢ coprime (a ^ n) b ↔ coprime a b
obtain ⟨n, rfl⟩ := exists_eq_succ_of_ne_zero hn.ne'
case intro
a b n : ℕ
hn : 0 < succ n
⊢ coprime (a ^ n) b ∧ coprime a b ↔ coprime a b
case intro
a b n : ℕ
hn : 0 < succ n
⊢ coprime (a ^ succ n) b ↔ coprime a b
rw [pow_succ, Nat.coprime_mul_iff_left]
no goals
case intro
a b n : ℕ
hn : 0 < succ n
⊢ coprime (a ^ n) b ∧ coprime a b ↔ coprime a b
exact ⟨And.right, fun hab => ⟨hab.pow_left _, hab⟩⟩