Theorem: Nat.size_succ_eq_succ_log_succ (Lib.lean)

State before:
n : ℕ
⊢ size (n + 1) = log 2 (n + 1) + 1
Tactic:
rw [← Nat.pred_size_eq_log, Nat.sub_add_cancel]
State after:
n : ℕ
⊢ 1 ≤ size (n + 1)

State before:
n : ℕ
⊢ 1 ≤ size (n + 1)
Tactic:
exact tsub_add_cancel_iff_le.mp rfl
State after:
no goals