WithBot ℕ

Lemmas about the type of natural numbers with a bottom element adjoined.

@[instance_reducible]

instance Nat.WithBot.instWellFoundedRelationWithBot : WellFoundedRelation (WithBot ℕ)

Equations

• Nat.WithBot.instWellFoundedRelationWithBot = { rel := fun (x1 x2 : WithBot ℕ) => x1 < x2, wf := Nat.WithBot.instWellFoundedRelationWithBot._proof_1 }

theorem Nat.WithBot.add_eq_zero_iff {n m : WithBot ℕ} : n + m = 0 ↔ n = 0 ∧ m = 0

theorem Nat.WithBot.add_eq_one_iff {n m : WithBot ℕ} : n + m = 1 ↔ n = 0 ∧ m = 1 ∨ n = 1 ∧ m = 0

theorem Nat.WithBot.add_eq_two_iff {n m : WithBot ℕ} : n + m = 2 ↔ n = 0 ∧ m = 2 ∨ n = 1 ∧ m = 1 ∨ n = 2 ∧ m = 0

theorem Nat.WithBot.add_eq_three_iff {n m : WithBot ℕ} : n + m = 3 ↔ n = 0 ∧ m = 3 ∨ n = 1 ∧ m = 2 ∨ n = 2 ∧ m = 1 ∨ n = 3 ∧ m = 0

theorem Nat.WithBot.coe_nonneg {n : ℕ} : 0 ≤ ↑n

@[simp]

theorem Nat.WithBot.lt_zero_iff {n : WithBot ℕ} : n < 0 ↔ n = ⊥

theorem Nat.WithBot.one_le_iff_zero_lt {x : WithBot ℕ} : 1 ≤ x ↔ 0 < x

theorem Nat.WithBot.lt_one_iff_le_zero {x : WithBot ℕ} : x < 1 ↔ x ≤ 0

theorem Nat.WithBot.add_one_le_of_lt {n m : WithBot ℕ} (h : n < m) : n + 1 ≤ m