Commit 2024-07-17 05:02 1e253566
View on Github →chore(Init/Data/Nat/Lemmas): remove more bit01 lemmas (#14788) Deletions:
- bit0_eq_zero
- bit0_inj
- bit0_le
- bit0_le_bit
- bit0_le_bit1_iff
- bit0_lt
- bit0_lt_bit0
- bit0_lt_bit1
- bit0_lt_bit1_iff
- bit0_ne
- bit0_ne_bit1
- bit0_ne_one
- bit1_eq_succ_bit0
- bit1_inj
- bit1_le
- bit1_le_bit0_iff
- bit1_lt
- bit1_lt_bit0
- bit1_lt_bit0_iff
- bit1_ne
- bit1_ne_bit0
- bit1_ne_one
- bit1_succ_eq
- bit_le_bit1
- bit_lt_bit0
- one_le_bit0
- one_le_bit1
- one_lt_bit0
- one_lt_bit1
- one_ne_bit0
- one_ne_bit1
- zero_ne_bit0
- zero_ne_bit1