This file contains convenience theorems around natural numbers. Right now, it only features prop_for_nat_has_minimal_such_nat.

@[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.