. apply Nat.dvd_sub'
  . trans ulp n a
    . exact ulp_dvd_ulp n hba
    . exact ulp_dvd_of_trunc_eq hfa
  . exact ulp_dvd_of_trunc_eq hfb
case hdvd
n a b : ℕ
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hab : a ≤ b + b
⊢ ulp n b ∣ a - b
no goals