rw [dvd_iff_multiplicity_le ha, dvd_iff_multiplicity_le ha']
case neg
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁴ : Field K
inst✝³ : CharZero K
inst✝² : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
M : Type u_2
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : UniqueFactorizationMonoid M
a b : M
x : ℕ
h' : x ≠ 0
ha : ¬a = 0
ha' : a ^ x ≠ 0
⊢ a ^ x ∣ b ^ x ↔ a ∣ b
case neg
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁴ : Field K
inst✝³ : CharZero K
inst✝² : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
M : Type u_2
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : UniqueFactorizationMonoid M
a b : M
x : ℕ
h' : x ≠ 0
ha : ¬a = 0
ha' : a ^ x ≠ 0
⊢ (∀ (p : M), Prime p → multiplicity p (a ^ x) ≤ multiplicity p (b ^ x)) ↔
    ∀ (p : M), Prime p → multiplicity p a ≤ multiplicity p b