Preliminaries #
noncomputable def
Nat.div2Induction
{motive : Nat → Sort u}
(n : Nat)
(ind : (n : Nat) → (n > 0 → motive (n / 2)) → motive n)
:
motive n
An induction principal that works on divison by two.
Equations
- Nat.div2Induction n ind = Nat.strongInductionOn n fun (n : Nat) (hyp : (m : Nat) → m < n → motive m) => ind n fun (n_pos : n > 0) => if n_eq : n = 0 then ⋯.elim else hyp (n / 2) ⋯
Instances For
testBit #
theorem
Nat.eq_of_testBit_eq
{x : Nat}
{y : Nat}
(pred : ∀ (i : Nat), x.testBit i = y.testBit i)
:
x = y
eq_of_testBit_eq
allows proving two natural numbers are equal
if their bits are all equal.
testBit 1 i
is true iff the index i
equals 0.