Theorem: round_eq_of_trunc_eq (Fl/Round.lean)

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