exact Int.eq_of_associated_of_nonneg hxy (hf' x hx) (factorsOddPrimeOrFour.nonneg hy)
a : ℤ
f : Multiset ℤ
hf : ∀ (x : ℤ), x ∈ f → OddPrimeOrFour x
hf' : ∀ (x : ℤ), x ∈ f → 0 ≤ x
ha : 0 < a
heven : Even (evenFactorExp a)
hassoc : Associated (Multiset.prod f) a
x : ℤ
hx : x ∈ f
y : ℤ
hy : y ∈ factorsOddPrimeOrFour a
hxy : Associated x y
⊢ x = y
no goals