Theorem: trunc_eq_self_of_uflow (Fl/Trunc.lean)

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

State before:
n x : ℕ
uflow : x < 2 ^ n
⊢ x / ulp n x * ulp n x = x
Tactic:
rw [ulp_eq_one_of_uflow uflow, Nat.mul_one, Nat.div_one]
State after:
no goals