cases Nat.lt_or_eq_of_le h with
| inl lt => have pos := Nat.zero_lt_of_lt lt
  rewrite [← next_trunc_pred_trunc_eq_self npos pos]
  apply Nat.le_trans
  . exact round_le_next_trunc hfaithful₁ y
  . apply next_le_next
    apply trunc_le_trunc npos
    apply Nat.le_pred_of_lt
    exact lt
| inr eq => rw [eq, round_trunc npos x hfaithful₀]
n x y : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
h : y ≤ trunc n x
⊢ round y ≤ trunc n x
no goals