cases eq_or_ne x 0 with
| inl eq_zero =>
  unfold trunc ulp expt
  rw [eq_zero, Nat.mul_zero, Nat.zero_div, Nat.zero_mul, Nat.mul_zero]
| inr ne_zero =>
  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)]
n : ℕ
npos : 0 < n
x k : ℕ
⊢ trunc n (2 ^ k * x) = 2 ^ k * trunc n x
no goals