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

State before:
⊢ log2RU 0 ≤ 0
Tactic:
decide
State after:
no goals

State before:
⊢ log2RU 1 ≤ 1
Tactic:
decide
State after:
no goals

State before:
n : Nat
⊢ log2RU (n + 2) ≤ n + 2
Tactic:
dsimp [log2RU]
State after:
n : Nat
⊢ log2' (2 * (n + 2 - 1)) ≤ n + 2

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

State before:
n : Nat
⊢ log2' (n + 1) + 1 ≤ n + 2
Tactic:
suffices log2' (n+1) ≤ n+1
  from Nat.succ_le_succ this
State after:
n : Nat
⊢ log2' (n + 1) ≤ n + 1

State before:
n : Nat
⊢ log2' (n + 1) ≤ n + 1
Tactic:
exact Nat.log2'_le_self _
State after:
no goals