case inl h =>
  cases h; dsimp [shiftRight]
  exact Nat.div_lt_self (Nat.zero_lt_of_ne_zero hn) (Nat.lt_succ_self 1)
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