. exact ulp_dvd_of_trunc_eq hfa
case h.h₁
n a b : ℕ
npos : 0 < n
hfa : trunc n a = a
le_ulp : b ≤ ulp n a
size_lt : 2 ^ (Nat.size a - 1) < a
⊢ ulp n a ∣ a

case h.h₂
n a b : ℕ
npos : 0 < n
hfa : trunc n a = a
le_ulp : b ≤ ulp n a
size_lt : 2 ^ (Nat.size a - 1) < a
⊢ ulp n a ∣ 2 ^ (Nat.size a - 1)

case h.h₃
n a b : ℕ
npos : 0 < n
hfa : trunc n a = a
le_ulp : b ≤ ulp n a
size_lt : 2 ^ (Nat.size a - 1) < a
⊢ 2 ^ (Nat.size a - 1) < a
case h.h₂
n a b : ℕ
npos : 0 < n
hfa : trunc n a = a
le_ulp : b ≤ ulp n a
size_lt : 2 ^ (Nat.size a - 1) < a
⊢ ulp n a ∣ 2 ^ (Nat.size a - 1)

case h.h₃
n a b : ℕ
npos : 0 < n
hfa : trunc n a = a
le_ulp : b ≤ ulp n a
size_lt : 2 ^ (Nat.size a - 1) < a
⊢ 2 ^ (Nat.size a - 1) < a