apply div_mul_pred_eq_sub_of_pos_of_dvd
x n : ℕ
xpos : 0 < x
hfx : trunc n x = x
⊢ (x - 1) / ulp n (x - 1) * ulp n (x - 1) = x - ulp n (x - 1)
case h₀
x n : ℕ
xpos : 0 < x
hfx : trunc n x = x
⊢ 0 < ulp n (x - 1)

case h₂
x n : ℕ
xpos : 0 < x
hfx : trunc n x = x
⊢ 0 < x

case h₁
x n : ℕ
xpos : 0 < x
hfx : trunc n x = x
⊢ ulp n (x - 1) ∣ x