Theorem: oddFactors.not_two_mem (Flt/OddPrimeOrFour.lean)

State before:
x : ℤ
⊢ ¬2 ∈ oddFactors x
Tactic:
simp only [oddFactors, even_bit0, not_true, not_false_iff, Int.odd_iff_not_even, and_false_iff,
  Multiset.mem_filter]
State after:
no goals