α : Type u_1
inst✝¹ : Ring α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
p a b : α
h : multiplicity p b < multiplicity p a
⊢ multiplicity p b < multiplicity p a
α : Type u_1
inst✝¹ : Ring α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
p a b : α
h : multiplicity p b < multiplicity p a
⊢ multiplicity p (a - b) = multiplicity p b
rw [sub_eq_add_neg, multiplicity_add_of_gt] <;> rw [multiplicity.neg]
no goals
α : Type u_1
inst✝¹ : Ring α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
p a b : α
h : multiplicity p b < multiplicity p a
⊢ multiplicity p b < multiplicity p a
assumption