n : ℕ
⊢ shiftr 0 n = 0
⊢ ∀ (n : ℕ), shiftr 0 n = 0
intro n
case zero

⊢ shiftr 0 zero = 0

case succ
n : ℕ
IH : shiftr 0 n = 0
⊢ shiftr 0 (succ n) = 0
n : ℕ
⊢ shiftr 0 n = 0
induction' n with n IH
case succ
n : ℕ
IH : shiftr 0 n = 0
⊢ shiftr 0 (succ n) = 0
case zero

⊢ shiftr 0 zero = 0

case succ
n : ℕ
IH : shiftr 0 n = 0
⊢ shiftr 0 (succ n) = 0
case zero =>
  rw [shiftr]
no goals
case succ
n : ℕ
IH : shiftr 0 n = 0
⊢ shiftr 0 (succ n) = 0
case succ =>
  rw [shiftr, div2, IH]
  rfl
no goals
⊢ shiftr 0 zero = 0
rw [shiftr]
n : ℕ
IH : shiftr 0 n = 0
⊢ (boddDiv2 0).snd = 0
n : ℕ
IH : shiftr 0 n = 0
⊢ shiftr 0 (succ n) = 0
rw [shiftr, div2, IH]
no goals
n : ℕ
IH : shiftr 0 n = 0
⊢ (boddDiv2 0).snd = 0
rfl