trans ulp n a
case hdvd.h₁
n a b : ℕ
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hab : a ≤ b + b
⊢ ulp n b ∣ a
n a b : ℕ
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hab : a ≤ b + b
⊢ ulp n b ∣ ulp n a

n a b : ℕ
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hab : a ≤ b + b
⊢ ulp n a ∣ a