Theorem: LO.FirstOrder.Derivation.ne_step_max' (Logic/FirstOrder/Basic/Calculus.lean)

State before:
L : Language
Δ Δ₁ Δ₂ Γ : Sequent L
p q r : SyntacticFormula L
n m : ℕ
⊢ n ≤ max m n
Tactic:
simp
State after:
no goals