Theorem: truncate_apply_of_le (Bruhat/Lehmer.lean)

State before:
f : ℕ → ℕ
n x : ℕ
hx : n ≤ x
⊢ ¬x < n
Tactic:
simpa
State after:
no goals