Theorem: ulp_eq_one_of_uflow (Fl/Trunc.lean)

State before:
n x : ℕ
uflow : x < 2 ^ n
⊢ ulp n x = 1
Tactic:
unfold ulp
State after:
n x : ℕ
uflow : x < 2 ^ n
⊢ 2 ^ expt n x = 1

State before:
n x : ℕ
uflow : x < 2 ^ n
⊢ 2 ^ expt n x = 1
Tactic:
rw [expt_eq_zero_of_uflow uflow, Nat.pow_zero]
State after:
no goals