case succ k h_ind=>
  conv => lhs; change (n >>> k) / 2
  calc
    (n >>> k) / 2 ≤ n >>> k := Nat.div_le_self _ 2
    _             ≤ n := h_ind
n k : Nat
h_ind : n >>> k ≤ n
⊢ n >>> succ k ≤ n
no goals