Theorem: trunc_idempotent (Fl/Trunc.lean)

State before:
n : ℕ
npos : 0 < n
x : ℕ
⊢ trunc n (trunc n x) = trunc n x
Tactic:
rw [trunc, ulp_trunc npos, trunc, Nat.mul_div_cancel _ (ulp_pos _ _)]
State after:
no goals