α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
s t : Associates α
d : Associates α
eq : t = s * d
⊢ factors s ≤ factors s + factors d
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
s t : Associates α
d : Associates α
eq : t = s * d
⊢ factors s ≤ factors t
rw [eq, factors_mul]
no goals
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
s t : Associates α
d : Associates α
eq : t = s * d
⊢ factors s ≤ factors s + factors d
exact le_add_of_nonneg_right bot_le