rewrite [ulp_eq_ulp]
case inr
n x y : ℕ
npos : 0 < n
h : x ≤ y
size_ge_size : Nat.size x ≥ Nat.size y
ulp_eq_ulp : ulp n x = ulp n y
⊢ x / ulp n x * ulp n x ≤ y / ulp n y * ulp n y
case inr
n x y : ℕ
npos : 0 < n
h : x ≤ y
size_ge_size : Nat.size x ≥ Nat.size y
ulp_eq_ulp : ulp n x = ulp n y
⊢ x / ulp n y * ulp n y ≤ y / ulp n y * ulp n y