Theorem: trunc_next_of_no_carry (Fl/Trunc.lean)

State before:
n x : ℕ
no_carry : next n x < 2 ^ Nat.size x
⊢ trunc n (next n x) = trunc n x + ulp n x
Tactic:
rw [trunc, ulp_next_of_no_carry no_carry, next, trunc, ← Nat.succ_mul,
    Nat.add_div_right _ (ulp_pos n x)]
State after:
no goals