Theorem: ulp_le_self (Fl/Trunc.lean)

State before:
n x : ℕ
npos : 0 < n
xpos : 0 < x
⊢ ulp n x ≤ x
Tactic:
unfold ulp expt
State after:
n x : ℕ
npos : 0 < n
xpos : 0 < x
⊢ 2 ^ (Nat.size x - n) ≤ x

State before:
n x : ℕ
npos : 0 < n
xpos : 0 < x
⊢ 2 ^ (Nat.size x - n) ≤ x
Tactic:
trans 2 ^ (Nat.size x - 1)
State after:
n x : ℕ
npos : 0 < n
xpos : 0 < x
⊢ 2 ^ (Nat.size x - n) ≤ 2 ^ (Nat.size x - 1)

n x : ℕ
npos : 0 < n
xpos : 0 < x
⊢ 2 ^ (Nat.size x - 1) ≤ x

State before:
n x : ℕ
npos : 0 < n
xpos : 0 < x
⊢ 2 ^ (Nat.size x - n) ≤ 2 ^ (Nat.size x - 1)

n x : ℕ
npos : 0 < n
xpos : 0 < x
⊢ 2 ^ (Nat.size x - 1) ≤ x
Tactic:
. apply Nat.pow_le_pow_of_le_right two_pos
  exact tsub_le_tsub_left (Nat.one_le_of_lt npos) _
State after:
n x : ℕ
npos : 0 < n
xpos : 0 < x
⊢ 2 ^ (Nat.size x - 1) ≤ x

State before:
n x : ℕ
npos : 0 < n
xpos : 0 < x
⊢ 2 ^ (Nat.size x - 1) ≤ x
Tactic:
. exact le_size_of_pos xpos
State after:
no goals

State before:
n x : ℕ
npos : 0 < n
xpos : 0 < x
⊢ 2 ^ (Nat.size x - n) ≤ 2 ^ (Nat.size x - 1)
Tactic:
apply Nat.pow_le_pow_of_le_right two_pos
State after:
n x : ℕ
npos : 0 < n
xpos : 0 < x
⊢ Nat.size x - n ≤ Nat.size x - 1

State before:
n x : ℕ
npos : 0 < n
xpos : 0 < x
⊢ Nat.size x - n ≤ Nat.size x - 1
Tactic:
exact tsub_le_tsub_left (Nat.one_le_of_lt npos) _
State after:
no goals

State before:
n x : ℕ
npos : 0 < n
xpos : 0 < x
⊢ 2 ^ (Nat.size x - 1) ≤ x
Tactic:
exact le_size_of_pos xpos
State after:
no goals