Cast of natural numbers: lemmas about bundled ordered semirings

@[simp]

theorem Nat.cast_nonneg {α : Type u_3} [OrderedSemiring α] (n : ℕ) : 0 ≤ ↑n

Specialisation of Nat.cast_nonneg', which seems to be easier for Lean to use.

@[simp]

theorem Nat.ofNat_nonneg {α : Type u_3} [OrderedSemiring α] (n : ℕ) [n.AtLeastTwo] : 0 ≤ OfNat.ofNat n

Specialisation of Nat.ofNat_nonneg', which seems to be easier for Lean to use.

@[simp]

theorem Nat.cast_min {α : Type u_3} [LinearOrderedSemiring α] {a : ℕ} {b : ℕ} : ↑(min a b) = min ↑a ↑b

@[simp]

theorem Nat.cast_max {α : Type u_3} [LinearOrderedSemiring α] {a : ℕ} {b : ℕ} : ↑(max a b) = max ↑a ↑b

@[simp]

theorem Nat.cast_pos {α : Type u_3} [OrderedSemiring α] [Nontrivial α] {n : ℕ} : 0 < ↑n ↔ 0 < n

Specialisation of Nat.cast_pos', which seems to be easier for Lean to use.

@[simp]

theorem Nat.ofNat_pos' {α : Type u_1} [AddMonoidWithOne α] [PartialOrder α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] [ZeroLEOneClass α] [NeZero 1] {n : ℕ} [n.AtLeastTwo] : 0 < OfNat.ofNat n

See also Nat.ofNat_pos, specialised for an OrderedSemiring.

@[simp]

theorem Nat.ofNat_pos {α : Type u_3} [OrderedSemiring α] [Nontrivial α] {n : ℕ} [n.AtLeastTwo] : 0 < OfNat.ofNat n

Specialisation of Nat.ofNat_pos', which seems to be easier for Lean to use.

@[simp]

theorem Nat.cast_tsub {α : Type u_1} [CanonicallyOrderedCommSemiring α] [Sub α] [OrderedSub α] [ContravariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] (m : ℕ) (n : ℕ) : ↑(m - n) = ↑m - ↑n

A version of Nat.cast_sub that works for ℝ≥0 and ℚ≥0. Note that this proof doesn't work for ℕ∞ and ℝ≥0∞, so we use type-specific lemmas for these types.

@[simp]

theorem Nat.abs_cast {α : Type u_1} [LinearOrderedRing α] (a : ℕ) : |↑a| = ↑a

@[simp]

theorem Nat.abs_ofNat {α : Type u_1} [LinearOrderedRing α] (n : ℕ) [n.AtLeastTwo] : |OfNat.ofNat n| = OfNat.ofNat n