(2 * k + 1) / 2 = k

Stream: new members

[Donald Sebastian Leung]

Given a natural number k, is there a quick way to show (2 * k + 1) / 2 = k in Lean? Perhaps I've simply not looked hard enough, but I've browsed through the mathlib docs for lemmas on / and div2 and none of them seem to directly imply my desired result.

[Mario Carneiro]

I believe there is a proof that div2 (bit1 k) = k

[Donald Sebastian Leung]

Oh, I see it now. I definitely haven't been looking hard enough :upside_down:

[Mario Carneiro]

alternatively, you can use the method used in that proof, via nat.add_mul_div_left and reflexivity to prove 1 / 2 = 0

[Kenny Lau]

import tactic.omega

example (n : ℕ) : (2 * n + 1) / 2 = n :=
nat.div_eq_of_lt_le (by omega) (by omega)