Theorem: trunc_add_half_ulp_eq_of_no_uflow (Fl/Trunc.lean)

State before:
n x : ℕ
npos : 0 < n
no_uflow : 2 ^ n ≤ x
⊢ 2 * (trunc n x + ulp n x / 2) = trunc n x + next n (trunc n x)
Tactic:
have ulp_even := two_dvd_ulp_of_no_uflow no_uflow
State after:
n x : ℕ
npos : 0 < n
no_uflow : 2 ^ n ≤ x
ulp_even : 2 ∣ ulp n x
⊢ 2 * (trunc n x + ulp n x / 2) = trunc n x + next n (trunc n x)

State before:
n x : ℕ
npos : 0 < n
no_uflow : 2 ^ n ≤ x
ulp_even : 2 ∣ ulp n x
⊢ 2 * (trunc n x + ulp n x / 2) = trunc n x + next n (trunc n x)
Tactic:
rw [Nat.left_distrib, Nat.two_mul, Nat.add_assoc,
    Nat.mul_div_cancel' ulp_even, ← ulp_trunc npos, next]
State after:
no goals