Theorem: ulp_trunc (Fl/Trunc.lean)

State before:
n : ℕ
npos : 0 < n
x : ℕ
⊢ ulp n (trunc n x) = ulp n x
Tactic:
unfold ulp expt
State after:
n : ℕ
npos : 0 < n
x : ℕ
⊢ 2 ^ (Nat.size (trunc n x) - n) = 2 ^ (Nat.size x - n)

State before:
n : ℕ
npos : 0 < n
x : ℕ
⊢ 2 ^ (Nat.size (trunc n x) - n) = 2 ^ (Nat.size x - n)
Tactic:
rw [size_trunc_eq_size npos x]
State after:
no goals