@[irreducible]

theorem prop_for_nat_has_minimal_such_nat (prop : Nat → Prop) (i : Nat) : prop i → ∃ (i : Nat), prop i ∧ ∀ (j : Fin i), ¬prop ↑j

if a there is a natural number such that a certain property holds, then there is a smallest such number.