Theorem: trunc_eq_sub_mod (Fl/Trunc.lean)

State before:
n x : ℕ
⊢ trunc n x = x - x % ulp n x
Tactic:
apply eq_tsub_of_add_eq
State after:
case h
n x : ℕ
⊢ trunc n x + x % ulp n x = x

State before:
case h
n x : ℕ
⊢ trunc n x + x % ulp n x = x
Tactic:
exact Nat.div_add_mod' x (ulp n x)
State after:
no goals