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

State before:
n k : Nat
⊢ n ≠ 0 → k > 0 → shiftRight n k < n
Tactic:
intro hn hk
State after:
n k : Nat
hn : n ≠ 0
hk : k > 0
⊢ shiftRight n k < n

State before:
n k : Nat
hn : n ≠ 0
hk : k > 0
⊢ shiftRight n k < n
Tactic:
induction k
State after:
case zero
n : Nat
hn : n ≠ 0
hk : zero > 0
⊢ shiftRight n zero < n

case succ
n : Nat
hn : n ≠ 0
n✝ : Nat
n_ih✝ : n✝ > 0 → shiftRight n n✝ < n
hk : succ n✝ > 0
⊢ shiftRight n (succ n✝) < n

State before:
n : Nat
hn : n ≠ 0
hk : zero > 0
⊢ shiftRight n zero < n
Tactic:
case zero => exact absurd hk (Nat.lt_irrefl 0)
State after:
no goals

State before:
n : Nat
hn : n ≠ 0
k : Nat
h_ind : k > 0 → shiftRight n k < n
hk : succ k > 0
⊢ shiftRight n (succ k) < n
Tactic:
case succ k h_ind =>
  unfold shiftRight
  cases Nat.eq_zero_or_pos k
  case inl h =>
    cases h; dsimp [shiftRight]
    exact Nat.div_lt_self (Nat.zero_lt_of_ne_zero hn) (Nat.lt_succ_self 1)
  case inr h =>
    calc
      shiftRight n k / 2
        ≤ shiftRight n k := Nat.div_le_self _ _
      _ < n := h_ind h
State after:
no goals

State before:
n : Nat
hn : n ≠ 0
hk : zero > 0
⊢ shiftRight n zero < n
Tactic:
exact absurd hk (Nat.lt_irrefl 0)
State after:
no goals

State before:
n : Nat
hn : n ≠ 0
k : Nat
h_ind : k > 0 → shiftRight n k < n
hk : succ k > 0
⊢ shiftRight n (succ k) < n
Tactic:
unfold shiftRight
State after:
n : Nat
hn : n ≠ 0
k : Nat
h_ind : k > 0 → shiftRight n k < n
hk : succ k > 0
⊢ shiftRight n k / 2 < n

State before:
n : Nat
hn : n ≠ 0
k : Nat
h_ind : k > 0 → shiftRight n k < n
hk : succ k > 0
⊢ shiftRight n k / 2 < n
Tactic:
cases Nat.eq_zero_or_pos k
State after:
case inl
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

case inr
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

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

State before:
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
Tactic:
case inr h =>
  calc
    shiftRight n k / 2
      ≤ shiftRight n k := Nat.div_le_self _ _
    _ < n := h_ind h
State after:
no goals

State before:
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
Tactic:
cases h
State after:
case refl
n : Nat
hn : n ≠ 0
h_ind : 0 > 0 → shiftRight n 0 < n
hk : succ 0 > 0
⊢ shiftRight n 0 / 2 < n

State before:
case refl
n : Nat
hn : n ≠ 0
h_ind : 0 > 0 → shiftRight n 0 < n
hk : succ 0 > 0
⊢ shiftRight n 0 / 2 < n
Tactic:
dsimp [shiftRight]
State after:
case refl
n : Nat
hn : n ≠ 0
h_ind : 0 > 0 → shiftRight n 0 < n
hk : succ 0 > 0
⊢ n / 2 < n

State before:
case refl
n : Nat
hn : n ≠ 0
h_ind : 0 > 0 → shiftRight n 0 < n
hk : succ 0 > 0
⊢ n / 2 < n
Tactic:
exact Nat.div_lt_self (Nat.zero_lt_of_ne_zero hn) (Nat.lt_succ_self 1)
State after:
no goals

State before:
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
Tactic:
calc
  shiftRight n k / 2
    ≤ shiftRight n k := Nat.div_le_self _ _
  _ < n := h_ind h
State after:
no goals