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 n m
Tactic:
simp
State after:
no goals