case intro
m c : ℤ
⊢ (2 * c + 1) / 2 * 2 + 1 = 2 * c + 1
m n : ℤ
⊢ Odd n → n / 2 * 2 + 1 = n
rintro ⟨c, rfl⟩
case h.e'_2.h.e'_6
m c : ℤ
⊢ 1 = (2 * c + 1) % 2
case intro
m c : ℤ
⊢ (2 * c + 1) / 2 * 2 + 1 = 2 * c + 1
convert Int.ediv_add_emod' (2 * c + 1) 2
no goals
case h.e'_2.h.e'_6
m c : ℤ
⊢ 1 = (2 * c + 1) % 2
simp [Int.add_emod]