theorem Nat.bit0_succ_eq (n : ℕ) : bit0 (Nat.succ n) = Nat.succ (Nat.succ (bit0 n))

theorem Nat.zero_lt_bit0 {n : ℕ} : n ≠ 0 → 0 < bit0 n

theorem Nat.zero_lt_bit1 (n : ℕ) : 0 < bit1 n

theorem Nat.bit0_ne_zero {n : ℕ} : n ≠ 0 → bit0 n ≠ 0

theorem Nat.bit1_ne_zero (n : ℕ) : bit1 n ≠ 0