Lean/Mathlib: FractionalIdeal.count equals DVR valuation of R_p without primary ideals

To identify Mathlib's FractionalIdeal.count K v (span {x}) with addVal of x in Localization.AtPrime v (Dedekind R), avoid proving x ∈ p^n ↔ n ≤ ord (needs p^n primary). Instead use rigidity: c(x) := count of span{x} is additive (span_singleton_mul_span_singleton, coeIdeal_mul, count_mul); c(s) = 0 for s ∉ p and c(t) = 1 for a uniformizer t ∈ R both follow from Ideal.count_normalizedFactors_eq with n = 0, 1 (only needs t ∉ p², which is the easy direction: map into R_p, maximalIdeal² = span{t²}). Then any x ≠ 0 satisfies s·x = y·tⁿ with s, y ∉ p, forcing c(x) = n. count_coe gives Associates.count ... factors; convert to (normalizedFactors J).count v by copying the rw chain from maxPowDividing_eq_pow_multiset_count. Name clash: write Ideal.count_normalizedFactors_eq explicitly when UniqueFactorizationMonoid is open. For QuotientGroup on ClassGroup R (a def), rw [QuotientGroup.eq_one_iff] fails on the motive; use exact (QuotientGroup.eq_one_iff I).2 ⟨x, _⟩.