English
For any n and i, the i-th testBit of n equals the i-th element of the list n.bits, i.e., testBit n i = n.bits.getI i.
Русский
Для любых n и i i-й бит n равен i-му элементу списка n.bits: testBit(n,i)=n.bits.getI(i).
LaTeX
$$$ testBit(n,i) = n.bits.getI(i) $$$
Lean4
/-- The ith bit is the ith element of `n.bits`. -/
theorem testBit_eq_inth (n i : ℕ) : n.testBit i = n.bits.getI i := by
induction i generalizing n with
|
zero =>
simp only [testBit, shiftRight_zero, one_and_eq_mod_two, mod_two_of_bodd, bodd_eq_bits_head,
List.getI_zero_eq_headI]
cases List.headI (bits n) <;> rfl
| succ i ih =>
conv_lhs => rw [← bit_bodd_div2 n]
rw [testBit_bit_succ, ih n.div2, div2_bits_eq_tail]
cases n.bits <;> simp
