Zulip Chat Archive

Stream: new members

Topic: (2 * k + 1) / 2 = k


view this post on Zulip Donald Sebastian Leung (Apr 13 2020 at 07:35):

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.

view this post on Zulip Mario Carneiro (Apr 13 2020 at 07:37):

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

view this post on Zulip Donald Sebastian Leung (Apr 13 2020 at 07:38):

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

view this post on Zulip Mario Carneiro (Apr 13 2020 at 07:39):

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

view this post on Zulip Kenny Lau (Apr 13 2020 at 07:42):

import tactic.omega

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

Last updated: May 09 2021 at 18:17 UTC