cases Nat.lt_or_ge (Nat.size x) (Nat.size y) with
| inl size_lt_size =>
  rewrite [← size_trunc_eq_size npos x] at size_lt_size
  rewrite [← size_trunc_eq_size npos y] at size_lt_size
  exact le_of_lt (lt_of_size_lt_size size_lt_size)
| inr size_ge_size =>
  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
  unfold trunc
  rewrite [ulp_eq_ulp]
  exact Nat.mul_le_mul_right _ (Nat.div_le_div_right h)
n x y : ℕ
npos : 0 < n
h : x ≤ y
⊢ trunc n x ≤ trunc n y
no goals