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

State before:
x✝ : 1 > 0
⊢ log2RU 1 < 1
Tactic:
decide
State after:
no goals

State before:
n : Nat
x✝ : n + 2 > 0
⊢ log2RU (n + 2) < n + 2
Tactic:
dsimp [log2RU]
State after:
n : Nat
x✝ : n + 2 > 0
⊢ log2' (2 * (n + 2 - 1)) < n + 2

State before:
n : Nat
x✝ : n + 2 > 0
⊢ log2' (2 * (n + 2 - 1)) < n + 2
Tactic:
simp [Nat.mul_add, log2'_div2]
State after:
n : Nat
x✝ : n + 2 > 0
⊢ log2' (n + 1) + 1 < n + 2

State before:
n : Nat
x✝ : n + 2 > 0
⊢ log2' (n + 1) + 1 < n + 2
Tactic:
suffices log2' (n+1) < n+1
  from Nat.succ_lt_succ this
State after:
n : Nat
x✝ : n + 2 > 0
⊢ log2' (n + 1) < n + 1

State before:
n : Nat
x✝ : n + 2 > 0
⊢ log2' (n + 1) < n + 1
Tactic:
exact Nat.log2'_lt_self (n+1) n.zero_lt_succ
State after:
no goals