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

State before:
k : Nat
⊢ 0 >>> k = 0
Tactic:
induction k
State after:
case zero

⊢ 0 >>> zero = 0

case succ
n✝ : Nat
n_ih✝ : 0 >>> n✝ = 0
⊢ 0 >>> succ n✝ = 0

State before:
⊢ 0 >>> zero = 0
Tactic:
case zero => rfl
State after:
no goals

State before:
k : Nat
h_ind : 0 >>> k = 0
⊢ 0 >>> succ k = 0
Tactic:
case succ k h_ind => rw [shiftRight_succ, h_ind]; rfl
State after:
no goals

State before:
⊢ 0 >>> zero = 0
Tactic:
rfl
State after:
no goals

State before:
k : Nat
h_ind : 0 >>> k = 0
⊢ 0 >>> succ k = 0
Tactic:
rw [shiftRight_succ, h_ind]
State after:
k : Nat
h_ind : 0 >>> k = 0
⊢ 0 / 2 = 0

State before:
k : Nat
h_ind : 0 >>> k = 0
⊢ 0 / 2 = 0
Tactic:
rfl
State after:
no goals