case succ l =>
  conv =>
    lhs; rw [Nat.mul_succ]; change (2*l+1+1-1)%2
    rw [Nat.add_sub_cancel, Nat.add_comm, Nat.add_mul_mod_self_left]
k : Nat
h_ind : ∀ (n : Nat), n &&& 2 ^ k - 1 = n % 2 ^ k
n l : Nat
hl : succ l > 0
⊢ (2 * succ l - 1) % 2 = 1
no goals