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