no goals
R : Type u_1
n✝ : ℕ
inst✝² : CommRing R
a b x✝ y✝ : R
p✝ : ℕ
inst✝¹ : IsDomain R
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
p : R
hp : Prime p
x y : R
hxy : p ∣ x - y
hx : ¬p ∣ x
n : ℕ
hn : ¬p ∣ ↑n
⊢ multiplicity p (x ^ n - y ^ n) = multiplicity p (x - y)
rw [← geom_sum₂_mul, multiplicity.mul hp, multiplicity_eq_zero.2 (not_dvd_geom_sum₂ hp hxy hx hn),
  zero_add]