no goals
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
p : Associates α
hp : ¬Irreducible p
s : FactorSet α
h : if hp : Irreducible p then BfactorSetMem { val := p, property := hp } s else False
⊢ False
rwa [dif_neg hp] at h