. apply Nat.dvd_sub'
  . rewrite [next, ulp_trunc npos]
    apply Nat.dvd_add
    . trans ulp n (a + b)
      . exact ulp_dvd_ulp n (Nat.le_add_left _ _)
      . exact ulp_dvd_trunc n _
    . exact ulp_dvd_ulp n (Nat.le_add_left _ _)
  . apply Nat.dvd_add
    . 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
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
lt_round : a + b < round (a + b)
ulp_sub_le : ulp n (a + b) - (a + b) % ulp n (a + b) ≤ b
⊢ ulp n b ∣ next n (trunc n (a + b)) - (a + b)
no goals