Theorem: trunc_sub_ulp_eq_of_trunc_eq (Fl/Trunc.lean)

State before:
n x : ℕ
npos : 0 < n
h : trunc n x = x
⊢ trunc n (x - ulp n x) = x - ulp n x
Tactic:
rewrite [← h, ulp_trunc npos]
State after:
n x : ℕ
npos : 0 < n
h : trunc n x = x
⊢ trunc n (trunc n x - ulp n x) = trunc n x - ulp n x

State before:
n x : ℕ
npos : 0 < n
h : trunc n x = x
⊢ trunc n (trunc n x - ulp n x) = trunc n x - ulp n x
Tactic:
exact trunc_trunc_sub_ulp_eq npos
State after:
no goals