cases Nat.lt_or_ge n (Nat.size x) with
| inr size_le =>
  have uflow : x < 2 ^ n := by
    rewrite [← Nat.size_le]
    exact size_le.le
  have d : ulp n (2 ^ k * x) ∣ 2 ^ k * x := by
    unfold ulp expt
    apply dvd_mul_of_dvd_left
    rewrite [Nat.pow_dvd_pow_iff_le_right one_lt_two]
    rewrite [size_pow_mul (Nat.zero_lt_of_ne_zero ne_zero)]
    rewrite [tsub_le_iff_left]
    apply Nat.add_le_add_right
    exact size_le
  rewrite [trunc_eq_self_of_uflow uflow]
  exact trunc_eq_of_le_of_ulp_dvd (2 ^ k * x) le_rfl d
| inl lt_size =>
  unfold trunc
  rewrite [ulp_pow_mul npos (le_of_lt lt_size)]
  rewrite [Nat.mul_div_mul_left _ _ two_pow_pos]
  rw [mul_rotate', Nat.mul_comm (ulp n x)]
case inr
n : ℕ
npos : 0 < n
x k : ℕ
ne_zero : x ≠ 0
⊢ trunc n (2 ^ k * x) = 2 ^ k * trunc n x
no goals