Theorem: lt_next_trunc (Fl/Trunc.lean)

State before:
n : ℕ
npos : 0 < n
x : ℕ
⊢ x < next n (trunc n x)
Tactic:
unfold next
State after:
n : ℕ
npos : 0 < n
x : ℕ
⊢ x < trunc n x + ulp n (trunc n x)

State before:
n : ℕ
npos : 0 < n
x : ℕ
⊢ x < trunc n x + ulp n (trunc n x)
Tactic:
rewrite [ulp_trunc npos]
State after:
n : ℕ
npos : 0 < n
x : ℕ
⊢ x < trunc n x + ulp n x

State before:
n : ℕ
npos : 0 < n
x : ℕ
⊢ x < trunc n x + ulp n x
Tactic:
unfold trunc
State after:
n : ℕ
npos : 0 < n
x : ℕ
⊢ x < x / ulp n x * ulp n x + ulp n x

State before:
n : ℕ
npos : 0 < n
x : ℕ
⊢ x < x / ulp n x * ulp n x + ulp n x
Tactic:
rewrite [← Nat.succ_mul, mul_comm]
State after:
n : ℕ
npos : 0 < n
x : ℕ
⊢ x < ulp n x * Nat.succ (x / ulp n x)

State before:
n : ℕ
npos : 0 < n
x : ℕ
⊢ x < ulp n x * Nat.succ (x / ulp n x)
Tactic:
exact Nat.lt_mul_div_succ x (ulp_pos n x)
State after:
no goals