α : Type u_1
inst✝¹ : Semiring α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
p a b : α
h : multiplicity p a ≤ multiplicity p b
⊢ ∀ (n : ℕ), p ^ n ∣ a → p ^ n ∣ a + b
α : Type u_1
inst✝¹ : Semiring α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
p a b : α
h : multiplicity p a ≤ multiplicity p b
⊢ min (multiplicity p a) (multiplicity p b) ≤ multiplicity p (a + b)
rw [min_eq_left h, multiplicity_le_multiplicity_iff]
no goals
α : Type u_1
inst✝¹ : Semiring α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
p a b : α
h : multiplicity p a ≤ multiplicity p b
⊢ ∀ (n : ℕ), p ^ n ∣ a → p ^ n ∣ a + b
exact fun n hn => dvd_add hn (multiplicity_le_multiplicity_iff.1 h n hn)
α : Type u_1
inst✝¹ : Semiring α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
p a b : α
h : multiplicity p b ≤ multiplicity p a
⊢ ∀ (n : ℕ), p ^ n ∣ b → p ^ n ∣ a + b
α : Type u_1
inst✝¹ : Semiring α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
p a b : α
h : multiplicity p b ≤ multiplicity p a
⊢ min (multiplicity p a) (multiplicity p b) ≤ multiplicity p (a + b)
rw [min_eq_right h, multiplicity_le_multiplicity_iff]
no goals
α : Type u_1
inst✝¹ : Semiring α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
p a b : α
h : multiplicity p b ≤ multiplicity p a
⊢ ∀ (n : ℕ), p ^ n ∣ b → p ^ n ∣ a + b
exact fun n hn => dvd_add (multiplicity_le_multiplicity_iff.1 h n hn) hn