Theorem: one_le_expt_of_no_uflow (Fl/Trunc.lean)

State before:
n x : ℕ
no_uflow : 2 ^ n ≤ x
⊢ 1 ≤ expt n x
Tactic:
unfold expt
State after:
n x : ℕ
no_uflow : 2 ^ n ≤ x
⊢ 1 ≤ Nat.size x - n

State before:
n x : ℕ
no_uflow : 2 ^ n ≤ x
⊢ 1 ≤ Nat.size x - n
Tactic:
apply le_tsub_of_add_le_left
State after:
case h
n x : ℕ
no_uflow : 2 ^ n ≤ x
⊢ n + 1 ≤ Nat.size x

State before:
case h
n x : ℕ
no_uflow : 2 ^ n ≤ x
⊢ n + 1 ≤ Nat.size x
Tactic:
rewrite [Nat.add_one, Nat.succ_le, Nat.lt_size]
State after:
case h
n x : ℕ
no_uflow : 2 ^ n ≤ x
⊢ 2 ^ n ≤ x

State before:
case h
n x : ℕ
no_uflow : 2 ^ n ≤ x
⊢ 2 ^ n ≤ x
Tactic:
exact no_uflow
State after:
no goals