theorem Nat.add_one_pos (n : ℕ) : 0 < n + 1

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

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