Cast of natural numbers: lemmas about bundled ordered semirings #

@[simp]
theorem Nat.cast_nonneg {α : Type u_3} [] (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} [] (n : ) [n.AtLeastTwo] :
0

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

@[simp]
theorem Nat.cast_min {α : Type u_3} {a : } {b : } :
(min a b) = min a b
@[simp]
theorem Nat.cast_max {α : Type u_3} {a : } {b : } :
(max a b) = max a b
@[simp]
theorem Nat.cast_pos {α : Type u_3} [] [] {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} [] [] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] [] [] {n : } [n.AtLeastTwo] :
0 <

See also Nat.ofNat_pos, specialised for an OrderedSemiring.

@[simp]
theorem Nat.ofNat_pos {α : Type u_3} [] [] {n : } [n.AtLeastTwo] :
0 <

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

@[simp]
theorem Nat.cast_tsub {α : Type u_1} [Sub α] [] [ContravariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] (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} (a : ) :
|a| = a
@[simp]
theorem Nat.abs_ofNat {α : Type u_1} (n : ) [n.AtLeastTwo] :
|| =
theorem Nat.mul_le_pow {a : } (ha : a 1) (b : ) :
a * b a ^ b