Theorem: next_trunc_sub_eq_ulp_sub_mod (Fl/Trunc.lean)

State before:
n : ℕ
npos : 0 < n
c : ℕ
⊢ next n (trunc n c) - c = ulp n c - c % ulp n c
Tactic:
unfold next
State after:
n : ℕ
npos : 0 < n
c : ℕ
⊢ trunc n c + ulp n (trunc n c) - c = ulp n c - c % ulp n c

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

State before:
n : ℕ
npos : 0 < n
c : ℕ
⊢ trunc n c + ulp n c - c = ulp n c - c % ulp n c
Tactic:
rewrite [trunc_eq_sub_mod]
State after:
n : ℕ
npos : 0 < n
c : ℕ
⊢ c - c % ulp n c + ulp n c - c = ulp n c - c % ulp n c

State before:
n : ℕ
npos : 0 < n
c : ℕ
⊢ c - c % ulp n c + ulp n c - c = ulp n c - c % ulp n c
Tactic:
rewrite [tsub_add_eq_add_tsub (Nat.mod_le _ _)]
State after:
n : ℕ
npos : 0 < n
c : ℕ
⊢ c + ulp n c - c % ulp n c - c = ulp n c - c % ulp n c

State before:
n : ℕ
npos : 0 < n
c : ℕ
⊢ c + ulp n c - c % ulp n c - c = ulp n c - c % ulp n c
Tactic:
rewrite [tsub_right_comm]
State after:
n : ℕ
npos : 0 < n
c : ℕ
⊢ c + ulp n c - c - c % ulp n c = ulp n c - c % ulp n c

State before:
n : ℕ
npos : 0 < n
c : ℕ
⊢ c + ulp n c - c - c % ulp n c = ulp n c - c % ulp n c
Tactic:
rw [add_tsub_cancel_left]
State after:
no goals