Theorem: trunc_round (Fl/Round.lean)

State before:
n : ℕ
npos : 0 < n
round : ℕ → ℕ
hfaithful₁ : faithful₁ n round
x : ℕ
⊢ trunc n (round x) = round x
Tactic:
cases hfaithful₁ x with
| inl lo => rw [lo, trunc_idempotent npos]
| inr hi => rw [hi, trunc_next_comm npos, trunc_idempotent npos]
State after:
no goals

State before:
case inl
n : ℕ
npos : 0 < n
round : ℕ → ℕ
hfaithful₁ : faithful₁ n round
x : ℕ
lo : round x = trunc n x
⊢ trunc n (round x) = round x
Tactic:
rw [lo, trunc_idempotent npos]
State after:
no goals

State before:
case inr
n : ℕ
npos : 0 < n
round : ℕ → ℕ
hfaithful₁ : faithful₁ n round
x : ℕ
hi : round x = next n (trunc n x)
⊢ trunc n (round x) = round x
Tactic:
rw [hi, trunc_next_comm npos, trunc_idempotent npos]
State after:
no goals