pith. machine review for the scientific record. sign in
lemma proved tactic proof

natToGray_testBit_false_of_ge

show as:
view Lean formalization →

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

generate prose now

formal statement (Lean)

 184private lemma natToGray_testBit_false_of_ge {d n k : Nat} (hn : n < 2 ^ d) (hk : d ≤ k) :
 185    (natToGray n).testBit k = false := by

proof body

Tactic-mode proof.

 186  -- natToGray n = n XOR (n >>> 1)
 187  have hn_lt : n < 2 ^ k := by
 188    have hpow : 2 ^ d ≤ 2 ^ k := by
 189      rcases lt_or_eq_of_le hk with hlt | rfl
 190      · exact le_of_lt (Nat.pow_lt_pow_right (by decide : 1 < (2 : Nat)) hlt)
 191      · rfl
 192    exact lt_of_lt_of_le hn hpow
 193  have hn_bit : n.testBit k = false := Nat.testBit_eq_false_of_lt hn_lt
 194  have hdiv_le : (n >>> 1) ≤ n := by
 195    -- shiftRight_eq_div_pow: n >>> 1 = n / 2
 196    simp [Nat.shiftRight_eq_div_pow, Nat.div_le_self]
 197  have hdiv_lt : (n >>> 1) < 2 ^ k := lt_of_le_of_lt hdiv_le hn_lt
 198  have hdiv_bit : (n >>> 1).testBit k = false := Nat.testBit_eq_false_of_lt hdiv_lt
 199  -- combine
 200  simp [natToGray, hn_bit, hdiv_bit]
 201
 202variable [GrayCodeFacts]
 203

used by (1)

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

depends on (2)

Lean names referenced from this declaration's body.