no goals
α : Type u_1
inst✝¹ : Monoid α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a b : α
k : ℕ
hk : a ^ k ∣ b
hsucc : ¬a ^ (k + 1) ∣ b
⊢ k = Part.get (multiplicity a b) (_ : ∃ n, (fun n => ¬a ^ (n + 1) ∣ b) n)
rw [← PartENat.natCast_inj, PartENat.natCast_get, unique hk hsucc]