. rewrite [ulp_trunc npos]
  unfold ulp expt
  apply Nat.pow_le_pow_of_le_right two_pos
  apply tsub_le_tsub_right
  rewrite [Nat.size_le]
  apply Nat.lt_of_lt_of_le k
  exact next_trunc_le npos x
case a
x y n : ℕ
npos : 0 < n
h : trunc n x ≤ y
k : y < next n (trunc n x)
⊢ ulp n y ≤ ulp n (trunc n x)
no goals