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

State before:
z a : ℤ
ha : a ∈ oddFactors z
⊢ 0 ≤ a
Tactic:
simp only [oddFactors, Multiset.mem_filter] at ha
State after:
z a : ℤ
ha : a ∈ UniqueFactorizationMonoid.normalizedFactors z ∧ Odd a
⊢ 0 ≤ a

State before:
z a : ℤ
ha : a ∈ UniqueFactorizationMonoid.normalizedFactors z ∧ Odd a
⊢ 0 ≤ a
Tactic:
exact
  Int.nonneg_of_normalize_eq_self (UniqueFactorizationMonoid.normalize_normalized_factor a ha.1)
State after:
no goals