Theorem: trunc_add_half_ulp_eq_of_uflow (Fl/Trunc.lean)

State before:
n x : ℕ
uflow : x < 2 ^ n
⊢ trunc n x + ulp n x / 2 = x
Tactic:
unfold trunc
State after:
n x : ℕ
uflow : x < 2 ^ n
⊢ x / ulp n x * ulp n x + ulp n x / 2 = x

State before:
n x : ℕ
uflow : x < 2 ^ n
⊢ x / ulp n x * ulp n x + ulp n x / 2 = x
Tactic:
rewrite [ulp_eq_one_of_uflow uflow]
State after:
n x : ℕ
uflow : x < 2 ^ n
⊢ x / 1 * 1 + 1 / 2 = x

State before:
n x : ℕ
uflow : x < 2 ^ n
⊢ x / 1 * 1 + 1 / 2 = x
Tactic:
rw [Nat.mul_one, Nat.div_one, Nat.div_eq_of_lt one_lt_two, Nat.add_zero]
State after:
no goals