case succ k h_ind =>
  unfold shiftRight
  cases Nat.eq_zero_or_pos k
  case inl h =>
    cases h; dsimp [shiftRight]
    exact Nat.div_lt_self (Nat.zero_lt_of_ne_zero hn) (Nat.lt_succ_self 1)
  case inr h =>
    calc
      shiftRight n k / 2
        ≤ shiftRight n k := Nat.div_le_self _ _
      _ < n := h_ind h
n : Nat
hn : n ≠ 0
k : Nat
h_ind : k > 0 → shiftRight n k < n
hk : succ k > 0
⊢ shiftRight n (succ k) < n
no goals