lemma proved tactic proof

`allOnes_testBit_eq_false_at`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

 103private lemma allOnes_testBit_eq_false_at (t : Nat) : (allOnes t).testBit t = false := by

proof body

Tactic-mode proof.

 104  -- `allOnes t < 2^t`
 105  have hlt : allOnes t < 2 ^ t := by
 106    -- `2^t - 1 < 2^t` since `2^t > 0`
 107    simpa [allOnes] using Nat.sub_lt (pow_pos (by decide : 0 < (2 : Nat)) t) (by decide : 0 < 1)
 108  exact Nat.testBit_eq_false_of_lt hlt
 109

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

brgc_wrap_oneBitDiff in IndisputableMonolith.Patterns.GrayCycleGeneral decl_use

depends on (1)

Lean names referenced from this declaration's body.

allOnes in IndisputableMonolith.Patterns.GrayCycleGeneral decl_use