source
theorem Std.PRange.Nat.succ_eq {n : Nat} :
succ n = n + 1
source
theorem Std.PRange.Nat.toList_Rco_succ_succ {m n : Nat} :
((m + 1)...n + 1).toList = List.map (fun (x : Nat) => x + 1) (m...n).toList
source
@[deprecated Std.PRange.Nat.toList_Rco_succ_succ (since := "2025-08-22")]
theorem Std.PRange.Nat.ClosedOpen.toList_succ_succ {m n : Nat} :
((m + 1)...n + 1).toList = List.map (fun (x : Nat) => x + 1) (m...n).toList
source
@[simp]
theorem Std.PRange.Nat.size_Rcc {a b : Nat} :
(a...=b).size = b + 1 - a
source
@[simp]
theorem Std.PRange.Nat.size_Rco {a b : Nat} :
(a...b).size = b - a
source
@[simp]
theorem Std.PRange.Nat.size_Roc {a b : Nat} :
(a<...=b).size = b - a
source
@[simp]
theorem Std.PRange.Nat.size_Roo {a b : Nat} :
(a<...b).size = b - a - 1
source
@[simp]
theorem Std.PRange.Nat.size_Ric {b : Nat} :
(*...=b).size = b + 1
source
@[simp]
theorem Std.PRange.Nat.size_Rio {b : Nat} :
(*...b).size = b