m✝ n : ℕ
x✝ : Odd n
m : ℕ
hm : n = 2 * m + 1
⊢ (0 + 1 % 2) % 2 = 1
m✝ n : ℕ
x✝ : Odd n
m : ℕ
hm : n = 2 * m + 1
⊢ n % 2 = 1
rw [hm, add_mod, mul_mod_right]
no goals
m✝ n : ℕ
x✝ : Odd n
m : ℕ
hm : n = 2 * m + 1
⊢ (0 + 1 % 2) % 2 = 1
rfl
no goals
m n : ℕ
h : n % 2 = 1
⊢ n % 2 + 2 * (n / 2) = 2 * (n / 2) + 1
rw [h, add_comm]