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
h : k > 0
⊢ shiftRight n k / 2 < n
no goals