Theorem: next_trunc_le (Fl/Trunc.lean)

State before:
n : ℕ
npos : 0 < n
x : ℕ
⊢ next n (trunc n x) ≤ 2 ^ Nat.size x
Tactic:
rewrite [← trunc_next_comm npos]
State after:
n : ℕ
npos : 0 < n
x : ℕ
⊢ trunc n (next n x) ≤ 2 ^ Nat.size x

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