n m : ℕ
hm : n ≠ m
⊢ bodd (2 ^ n / 2 ^ m) = false
n m : ℕ
hm : n ≠ m
⊢ testBit (2 ^ n) m = false
rw [testBit, shiftr_eq_div_pow]
case inl
n m : ℕ
hm✝ : n ≠ m
hm : n < m
⊢ bodd (2 ^ n / 2 ^ m) = false

case inr
n m : ℕ
hm✝ : n ≠ m
hm : m < n
⊢ bodd (2 ^ n / 2 ^ m) = false
n m : ℕ
hm : n ≠ m
⊢ bodd (2 ^ n / 2 ^ m) = false
cases' hm.lt_or_lt with hm hm
case inl
n m : ℕ
hm✝ : n ≠ m
hm : n < m
⊢ 2 ^ n < 2 ^ m
case inl
n m : ℕ
hm✝ : n ≠ m
hm : n < m
⊢ bodd (2 ^ n / 2 ^ m) = false
rw [Nat.div_eq_zero, bodd_zero]
no goals
case inl
n m : ℕ
hm✝ : n ≠ m
hm : n < m
⊢ 2 ^ n < 2 ^ m
exact Nat.pow_lt_pow_of_lt_right one_lt_two hm
case inr
n m : ℕ
hm✝ : n ≠ m
hm : m < n
⊢ bodd (2 ^ (n - m - succ 0 + succ 0)) = false
case inr
n m : ℕ
hm✝ : n ≠ m
hm : m < n
⊢ bodd (2 ^ n / 2 ^ m) = false
rw [pow_div hm.le zero_lt_two, ← tsub_add_cancel_of_le (succ_le_of_lt <| tsub_pos_of_lt hm)]
case inr
n m : ℕ
hm✝ : n ≠ m
hm : m < n
⊢ bodd (2 ^ (n - m - succ 0 + succ 0)) = false
case inr
n m : ℕ
hm✝ : n ≠ m
hm : m < n
⊢ bodd (2 ^ (n - m - succ 0 + succ 0)) = false
rw [(rfl : succ 0 = 1)]
no goals
case inr
n m : ℕ
hm✝ : n ≠ m
hm : m < n
⊢ bodd (2 ^ (n - m - succ 0 + succ 0)) = false
simp only [ge_iff_le, tsub_le_iff_right, pow_succ, bodd_mul,
  Bool.and_eq_false_eq_eq_false_or_eq_false, or_true]