testBit_bit_succ — Mathlib

English

For any m, b, n: testBit(bit(b,n), m+1) = testBit(n, m).

Русский

Для любых m, b, n: testBit(bit(b,n), m+1) = testBit(n, m).

LaTeX

$$$$ \forall (m : \mathbb{N}) (b : \mathrm{Bool}) (n : \mathbb{N}), \; \mathrm{testBit}(\mathrm{bit}(b,n), m+1) = \mathrm{testBit}(n, m). $$$$

Lean4

theorem testBit_bit_succ (m b n) : testBit (bit b n) (succ m) = testBit n m :=
  by
  have : bodd (((bit b n) >>> 1) >>> m) = bodd (n >>> m) :=
    by
    simp only [shiftRight_eq_div_pow]
    simp [← div2_val, div2_bit]
  rw [← shiftRight_add, Nat.add_comm] at this
  simp only [bodd_eq_one_and_ne_zero] at this
  exact this

Похожие утверждения