exact dvd_mul_right _ _
p : ℤ
f : Multiset ℤ
ih :
  ∀ {g : Multiset ℤ},
    (∀ (x : ℤ), x ∈ f → OddPrimeOrFour x) →
      (∀ (x : ℤ), x ∈ g → OddPrimeOrFour x) →
        Associated (Multiset.prod f) (Multiset.prod g) → Multiset.Rel Associated f g
g : Multiset ℤ
hf : ∀ (x : ℤ), x ∈ p ::ₘ f → OddPrimeOrFour x
hg : ∀ (x : ℤ), x ∈ g → OddPrimeOrFour x
hfg : Associated (Multiset.prod (p ::ₘ f)) (Multiset.prod g)
hp : OddPrimeOrFour p
⊢ p ∣ p * Multiset.prod f
no goals