feat(data/nat/basic): simp-lemmas for bit0 and bit1 mod two (#4343)

Co-Authored-By: Gabriel Ebner <gebner@gebner.org>
leanprover-community · Oct 1, 2020 · f10dda0 · f10dda0
1 parent 0fc7b29
commit f10dda0
Showing 1 changed file with 4 additions and 0 deletions.
diff --git a/src/data/nat/basic.lean b/src/data/nat/basic.lean
@@ -1367,6 +1367,10 @@ by { convert bit1_lt_bit0_iff, refl, }
 | ff := bit0_le_bit1_iff
 | tt := bit1_le_bit1
 
+@[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 }
+
 lemma pos_of_bit0_pos {n : ℕ} (h : 0 < bit0 n) : 0 < n :=
 by { cases n, cases h, apply succ_pos, }