Theorem: Nat.ne_step_max' (Logic/Vorspiel/Vorspiel.lean)

State before:
α : ℕ → Sort u
n m : ℕ
⊢ n ≤ max m n
Tactic:
simp
State after:
no goals