apply Eq.symm
x y n : ℕ
npos : 0 < n
h : trunc n x ≤ y
k : y < next n (trunc n x)
ulp_eq : ulp n x = ulp n y
⊢ x / ulp n x * ulp n x = y / ulp n x * ulp n x
case h
x y n : ℕ
npos : 0 < n
h : trunc n x ≤ y
k : y < next n (trunc n x)
ulp_eq : ulp n x = ulp n y
⊢ y / ulp n x * ulp n x = x / ulp n x * ulp n x