Theorem: Misc.Nat.odd_iff (LeanSAT/Util/Misc.lean)

State before:
n : Nat
x✝ : Odd n
m : Nat
hm : n = 2 * m + 1
⊢ n % 2 = 1
Tactic:
rw [hm, Nat.add_mod, Nat.mul_mod_right]
State after:
no goals

State before:
n : Nat
h : n % 2 = 1
⊢ n % 2 + 2 * (n / 2) = 2 * (n / 2) + 1
Tactic:
rw [h, Nat.add_comm]
State after:
no goals