Theorem: size_next_le_succ_size (Fl/Trunc.lean)

State before:
n x : ℕ
⊢ Nat.size (next n x) ≤ Nat.size x + 1
Tactic:
rewrite [Nat.size_le, Nat.pow_succ, Nat.mul_two]
State after:
n x : ℕ
⊢ next n x < 2 ^ Nat.size x + 2 ^ Nat.size x

State before:
n x : ℕ
⊢ next n x < 2 ^ Nat.size x + 2 ^ Nat.size x
Tactic:
unfold next ulp
State after:
n x : ℕ
⊢ x + 2 ^ expt n x < 2 ^ Nat.size x + 2 ^ Nat.size x

State before:
n x : ℕ
⊢ x + 2 ^ expt n x < 2 ^ Nat.size x + 2 ^ Nat.size x
Tactic:
rewrite [Nat.add_comm, ← Nat.add_one_le_iff, add_rotate]
State after:
n x : ℕ
⊢ x + 1 + 2 ^ expt n x ≤ 2 ^ Nat.size x + 2 ^ Nat.size x

State before:
n x : ℕ
⊢ x + 1 + 2 ^ expt n x ≤ 2 ^ Nat.size x + 2 ^ Nat.size x
Tactic:
apply Nat.add_le_add
State after:
case h₁
n x : ℕ
⊢ x + 1 ≤ 2 ^ Nat.size x

case h₂
n x : ℕ
⊢ 2 ^ expt n x ≤ 2 ^ Nat.size x

State before:
case h₁
n x : ℕ
⊢ x + 1 ≤ 2 ^ Nat.size x

case h₂
n x : ℕ
⊢ 2 ^ expt n x ≤ 2 ^ Nat.size x
Tactic:
. exact Nat.lt_size_self x
State after:
case h₂
n x : ℕ
⊢ 2 ^ expt n x ≤ 2 ^ Nat.size x

State before:
case h₂
n x : ℕ
⊢ 2 ^ expt n x ≤ 2 ^ Nat.size x
Tactic:
. exact Nat.pow_le_pow_of_le_right two_pos tsub_le_self
State after:
no goals

State before:
case h₁
n x : ℕ
⊢ x + 1 ≤ 2 ^ Nat.size x
Tactic:
exact Nat.lt_size_self x
State after:
no goals

State before:
case h₂
n x : ℕ
⊢ 2 ^ expt n x ≤ 2 ^ Nat.size x
Tactic:
exact Nat.pow_le_pow_of_le_right two_pos tsub_le_self
State after:
no goals