## Stream: Is there code for X?

### Topic: bit mod two

#### Johan Commelin (Oct 01 2020 at 07:57):

Do we have these? I couldn't find them, but I'm a bit surprised.

namespace nat

variables (n : ℕ)

@[simp] lemma bit0_mod_two : bit0 n % 2 = 0 :=
show (n + n) % 2 = 0, by rw [← two_mul, mul_mod, mod_self, zero_mul, zero_mod]

@[simp] lemma bit1_mod_two : bit1 n % 2 = 1 :=

end nat


#### Gabriel Ebner (Oct 01 2020 at 08:09):

The closest I could find is bodd_bit:

variables (n : ℕ)

@[simp] lemma bodd_bit0 : (bit0 n).bodd = ff := nat.bodd_bit ff _
@[simp] lemma bodd_bit1 : (bit1 n).bodd = tt := nat.bodd_bit tt _
@[simp] lemma bit0_mod_two : bit0 n % 2 = 0 := by rw nat.mod_two_of_bodd; simp
@[simp] lemma bit1_mod_two : bit1 n % 2 = 1 := by rw nat.mod_two_of_bodd; simp


#### Johan Commelin (Oct 01 2020 at 08:27):

@Gabriel Ebner Thanks! You managed to prove twice as many simp-lemmas in about the same number of characters.

#### Johan Commelin (Oct 01 2020 at 08:29):

Shall I PR these to nat.basic?

#### Gabriel Ebner (Oct 01 2020 at 08:30):

Apparently bodd_bit0 is already in nat.basic. So yes, that seems like the right place.

#### Johan Commelin (Oct 01 2020 at 08:35):

#4343

Last updated: May 17 2021 at 15:13 UTC