calc
  b - ulp n b
  _ = trunc n (b - ulp n b) := Eq.symm $ trunc_sub_ulp_eq_of_trunc_eq npos hfb
  _ ≤ trunc n (b - a)       := trunc_le_trunc npos $ tsub_le_tsub_left le_ulp _
n a b : ℕ
npos : 0 < n
hfb : trunc n b = b
h : ulp n b ≤ 2 * a
le_ulp : a ≤ ulp n b
⊢ b - ulp n b ≤ trunc n (b - a)
no goals