Theorem: trunc_eq_of_round_eq (Fl/Round.lean)

State before:
n x : ℕ
npos : 0 < n
round : ℕ → ℕ
hfaithful₁ : faithful₁ n round
round_eq : round x = x
⊢ trunc n x = x
Tactic:
rw [← round_eq, trunc_round npos hfaithful₁ x]
State after:
no goals