Theorem: Int.odd_ne_zero (UnitConjecture/TorsionFree.lean)

State before:
⊢ ∀ (a : ℤ), ¬a + a + 1 = 0
Tactic:
intro a h
State after:
a : ℤ
h : a + a + 1 = 0
⊢ False

State before:
a : ℤ
h : a + a + 1 = 0
this : (a + a + 1) % 2 = 0 % 2
⊢ False
Tactic:
simp [Int.add_emod] at this
State after:
no goals