Theorem: le_size_of_pos (Fl/Lemmas.lean)

State before:
x : ℕ
pos : 0 < x
⊢ 2 ^ (Nat.size x - 1) ≤ x
Tactic:
rewrite [← Nat.lt_size]
State after:
x : ℕ
pos : 0 < x
⊢ Nat.size x - 1 < Nat.size x

State before:
x : ℕ
pos : 0 < x
⊢ Nat.size x - 1 < Nat.size x
Tactic:
exact tsub_lt_self (Nat.size_pos.mpr pos) one_pos
State after:
no goals