have ulp_eq_ulp : ulp n x = ulp n y := by
  apply congr_arg (fun w => 2 ^ (w - n))
  exact Nat.le_antisymm (Nat.size_le_size h) size_ge_size
case inr
n x y : ℕ
npos : 0 < n
h : x ≤ y
size_ge_size : Nat.size x ≥ Nat.size y
⊢ trunc n x ≤ trunc 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
⊢ trunc n x ≤ trunc n y