α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
p q : Associates α
hp : Irreducible p
hq : Irreducible q
h : p ≠ q
h' : count p (factors q) ≠ 0
✝ : Nontrivial α
⊢ p ∣ q
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
p q : Associates α
hp : Irreducible p
hq : Irreducible q
h : p ≠ q
h' : count p (factors q) ≠ 0
⊢ p ∣ q
nontriviality α
no goals
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
p q : Associates α
hp : Irreducible p
hq : Irreducible q
h : p ≠ q
h' : count p (factors q) ≠ 0
✝ : Nontrivial α
⊢ p ∣ q
exact le_of_count_ne_zero hq.ne_zero hp h'