Principle_of_Least_Counterexample
Provedproof-techniquesproofwiki
If not all integers n >= m satisfy P(n), then there is a least counterexample.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Principle_of_Least_Counterexample (P : ℤ → Prop) (m : ℤ) (h : ¬∀ n, m ≤ n → P n) : ∃ n, m ≤ n ∧ ¬P n ∧ ∀ k, m ≤ k → ¬P k → n ≤ k := by sorry
Source