. exact xpos
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
case h₁
x n : ℕ
xpos : 0 < x
hfx : trunc n x = x
⊢ ulp n (x - 1) ∣ x