Theorem: trunc_next_le (Fl/Trunc.lean)

State before:
n : ℕ
npos : 0 < n
x : ℕ
⊢ trunc n (next n x) ≤ 2 ^ Nat.size x
Tactic:
cases Nat.le_total (next n x) (2 ^ Nat.size x) with
| inl le => exact Nat.le_trans (trunc_le n (next n x)) le
| inr ge => exact Nat.le_of_eq (trunc_next_of_carry npos ge)
State after:
no goals

State before:
case inl
n : ℕ
npos : 0 < n
x : ℕ
le : next n x ≤ 2 ^ Nat.size x
⊢ trunc n (next n x) ≤ 2 ^ Nat.size x
Tactic:
exact Nat.le_trans (trunc_le n (next n x)) le
State after:
no goals

State before:
case inr
n : ℕ
npos : 0 < n
x : ℕ
ge : 2 ^ Nat.size x ≤ next n x
⊢ trunc n (next n x) ≤ 2 ^ Nat.size x
Tactic:
exact Nat.le_of_eq (trunc_next_of_carry npos ge)
State after:
no goals