Theorem: Nat.shiftRight_shiftRight (Algdata/Data/Nat/Bits.lean)

State before:
n k l : Nat
⊢ n >>> k >>> l = n >>> (k + l)
Tactic:
induction l
State after:
case zero
n k : Nat
⊢ n >>> k >>> zero = n >>> (k + zero)

case succ
n k n✝ : Nat
n_ih✝ : n >>> k >>> n✝ = n >>> (k + n✝)
⊢ n >>> k >>> succ n✝ = n >>> (k + succ n✝)

State before:
n k : Nat
⊢ n >>> k >>> zero = n >>> (k + zero)
Tactic:
case zero => rfl
State after:
no goals

State before:
n k l : Nat
h_ind : n >>> k >>> l = n >>> (k + l)
⊢ n >>> k >>> succ l = n >>> (k + succ l)
Tactic:
case succ l h_ind =>
  conv =>
    rw [add_succ, shiftRight_succ, shiftRight_succ, h_ind]
State after:
no goals

State before:
n k : Nat
⊢ n >>> k >>> zero = n >>> (k + zero)
Tactic:
rfl
State after:
no goals

State before:
n k l : Nat
h_ind : n >>> k >>> l = n >>> (k + l)
⊢ n >>> k >>> succ l = n >>> (k + succ l)
Tactic:
conv =>
  rw [add_succ, shiftRight_succ, shiftRight_succ, h_ind]
State after:
no goals