Theorem: Nat.shiftRight_le_self (Algdata/Init/Nat.lean)

State before:
n k : Nat
⊢ n >>> k ≤ n
Tactic:
induction k
State after:
case zero
n : Nat
⊢ n >>> zero ≤ n

case succ
n n✝ : Nat
n_ih✝ : n >>> n✝ ≤ n
⊢ n >>> succ n✝ ≤ n

State before:
n : Nat
⊢ n >>> zero ≤ n
Tactic:
case zero => exact Nat.le.refl
State after:
no goals

State before:
n k : Nat
h_ind : n >>> k ≤ n
⊢ n >>> succ k ≤ n
Tactic:
case succ k h_ind=>
  conv => lhs; change (n >>> k) / 2
  calc
    (n >>> k) / 2 ≤ n >>> k := Nat.div_le_self _ 2
    _             ≤ n := h_ind
State after:
no goals

State before:
n : Nat
⊢ n >>> zero ≤ n
Tactic:
exact Nat.le.refl
State after:
no goals

State before:
n k : Nat
h_ind : n >>> k ≤ n
⊢ n >>> succ k ≤ n
Tactic:
conv => lhs; change (n >>> k) / 2
State after:
n k : Nat
h_ind : n >>> k ≤ n
⊢ n >>> k / 2 ≤ n

State before:
n k : Nat
h_ind : n >>> k ≤ n
⊢ n >>> k / 2 ≤ n
Tactic:
calc
  (n >>> k) / 2 ≤ n >>> k := Nat.div_le_self _ 2
  _             ≤ n := h_ind
State after:
no goals