exact Multiset.mem_cons_of_mem this
case cons.inr
p : ℕ
hp : OddPrimeOrFour p
a : ℕ
s : Multiset ℕ
ih : (∀ r ∈ s, OddPrimeOrFour r) → p ∣ s.prod → p ∈ s
hs : ∀ r ∈ a ::ₘ s, OddPrimeOrFour r
hdvd : p ∣ a * s.prod
this✝ : OddPrimeOrFour a
h : p ∣ s.prod
this : p ∈ s
⊢ p ∈ a ::ₘ s
no goals