Theorem: trunc_next_comm (Fl/Trunc.lean)

State before:
n : ℕ
npos : 0 < n
x : ℕ
⊢ trunc n (next n x) = next n (trunc n x)
Tactic:
cases Nat.lt_or_ge (next n x) (2 ^ Nat.size x) with
| inl next_lt => exact trunc_next_comm_of_no_carry npos next_lt
| inr next_ge => rw [next_trunc_of_carry npos next_ge, trunc_next_of_carry npos next_ge]
State after:
no goals

State before:
case inl
n : ℕ
npos : 0 < n
x : ℕ
next_lt : next n x < 2 ^ Nat.size x
⊢ trunc n (next n x) = next n (trunc n x)
Tactic:
exact trunc_next_comm_of_no_carry npos next_lt
State after:
no goals

State before:
case inr
n : ℕ
npos : 0 < n
x : ℕ
next_ge : next n x ≥ 2 ^ Nat.size x
⊢ trunc n (next n x) = next n (trunc n x)
Tactic:
rw [next_trunc_of_carry npos next_ge, trunc_next_of_carry npos next_ge]
State after:
no goals