unfold shiftRight
n : Nat
hn : n ≠ 0
k : Nat
h_ind : k > 0 → shiftRight n k < n
hk : succ k > 0
⊢ shiftRight n (succ k) < n
n : Nat
hn : n ≠ 0
k : Nat
h_ind : k > 0 → shiftRight n k < n
hk : succ k > 0
⊢ shiftRight n k / 2 < n