Further lemmas about the natural numbers

The distinction between this file and Mathlib/Algebra/Order/Ring/Nat.lean is not particularly clear. They were separated for now to minimize the porting requirements for tactics during the transition to mathlib4. Please feel free to reorganize these two files.

Sets

instance Nat.Subtype.orderBot (s : Set ℕ) [DecidablePred fun (x : ℕ) => x ∈ s] [h : Nonempty ↑s] : OrderBot ↑s

Equations

• Nat.Subtype.orderBot s = { bot := ⟨Nat.find ⋯, ⋯⟩, bot_le := ⋯ }

instance Nat.Subtype.semilatticeSup (s : Set ℕ) : SemilatticeSup ↑s

Equations

• Nat.Subtype.semilatticeSup s = { toPartialOrder := LinearOrder.toPartialOrder, sup := SemilatticeSup.sup, le_sup_left := ⋯, le_sup_right := ⋯, sup_le := ⋯ }

theorem Nat.Subtype.coe_bot {s : Set ℕ} [DecidablePred fun (x : ℕ) => x ∈ s] [h : Nonempty ↑s] : ↑⊥ = Nat.find ⋯

theorem Nat.set_eq_univ {S : Set ℕ} : S = Set.univ ↔ 0 ∈ S ∧ ∀ k ∈ S, k + 1 ∈ S

theorem Nat.exists_not_and_succ_of_not_zero_of_exists {p : ℕ → Prop} (H' : ¬p 0) (H : ∃ (n : ℕ), p n) : ∃ (n : ℕ), ¬p n ∧ p (n + 1)