exact trunc_eq_of_le_of_ulp_dvd (2 ^ k * x) le_rfl d
case inr.inr
n : ℕ
npos : 0 < n
x k : ℕ
ne_zero : x ≠ 0
size_le : n ≥ Nat.size x
uflow : x < 2 ^ n
d : ulp n (2 ^ k * x) ∣ 2 ^ k * x
⊢ trunc n (2 ^ k * x) = 2 ^ k * x
no goals