dsimp [shiftRight]
case refl
n : Nat
hn : n ≠ 0
h_ind : 0 > 0 → shiftRight n 0 < n
hk : succ 0 > 0
⊢ shiftRight n 0 / 2 < n
case refl
n : Nat
hn : n ≠ 0
h_ind : 0 > 0 → shiftRight n 0 < n
hk : succ 0 > 0
⊢ n / 2 < n