Theorem: Nat.log2'_lt_self (Algdata/Data/Nat/Bits.lean)

State before:
n : Nat
⊢ n > 0 → log2' n < n
Tactic:
intro hpos
State after:
n : Nat
hpos : n > 0
⊢ log2' n < n

State before:
n : Nat
hpos : n > 0
⊢ log2' n < n
Tactic:
induction n using recBase2
State after:
case zero
hpos : 0 > 0
⊢ log2' 0 < 0

case one
hpos : 1 > 0
⊢ log2' 1 < 1

case div2
n✝ : Nat
a✝ : n✝ / 2 + 1 > 0 → log2' (n✝ / 2 + 1) < n✝ / 2 + 1
hpos : n✝ + 2 > 0
⊢ log2' (n✝ + 2) < n✝ + 2

State before:
hpos : 0 > 0
⊢ log2' 0 < 0
Tactic:
case zero => cases hpos
State after:
no goals

State before:
hpos : 1 > 0
⊢ log2' 1 < 1
Tactic:
case one => decide
State after:
no goals

State before:
n : Nat
h_ind : n / 2 + 1 > 0 → log2' (n / 2 + 1) < n / 2 + 1
hpos : n + 2 > 0
⊢ log2' (n + 2) < n + 2
Tactic:
case div2 n h_ind =>
  suffices log2' (n/2 + 1) < n+1
    from log2'_div2 n ▸ Nat.succ_lt_succ this
  calc
    log2' (n/2 + 1)
      < n/2 + 1 := h_ind (Nat.zero_lt_succ ..)
    _ ≤ n + 1 := Nat.succ_le_succ (Nat.div_le_self n 2)
State after:
no goals

State before:
hpos : 0 > 0
⊢ log2' 0 < 0
Tactic:
cases hpos
State after:
no goals

State before:
hpos : 1 > 0
⊢ log2' 1 < 1
Tactic:
decide
State after:
no goals

State before:
n : Nat
h_ind : n / 2 + 1 > 0 → log2' (n / 2 + 1) < n / 2 + 1
hpos : n + 2 > 0
⊢ log2' (n + 2) < n + 2
Tactic:
suffices log2' (n/2 + 1) < n+1
  from log2'_div2 n ▸ Nat.succ_lt_succ this
State after:
n : Nat
h_ind : n / 2 + 1 > 0 → log2' (n / 2 + 1) < n / 2 + 1
hpos : n + 2 > 0
⊢ log2' (n / 2 + 1) < n + 1

State before:
n : Nat
h_ind : n / 2 + 1 > 0 → log2' (n / 2 + 1) < n / 2 + 1
hpos : n + 2 > 0
⊢ log2' (n / 2 + 1) < n + 1
Tactic:
calc
  log2' (n/2 + 1)
    < n/2 + 1 := h_ind (Nat.zero_lt_succ ..)
  _ ≤ n + 1 := Nat.succ_le_succ (Nat.div_le_self n 2)
State after:
no goals