theorem Std.PRange.Nat.succ_eq {n : Nat} : succ n = n + 1

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

@[deprecated Std.PRange.Nat.toList_rco_succ_succ (since := "2025-10-30")]

def 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

Equations

• @Std.PRange.Nat.toList_Rco_succ_succ = @Std.PRange.Nat.toList_rco_succ_succ

@[deprecated Std.PRange.Nat.toList_rco_succ_succ (since := "2025-08-22")]

def 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

Equations

• @Std.PRange.Nat.ClosedOpen.toList_succ_succ = @Std.PRange.Nat.toList_rco_succ_succ

@[simp]

theorem Std.PRange.Nat.size_rcc {a b : Nat} : (a...=b).size = b + 1 - a

@[deprecated Std.PRange.Nat.size_rcc (since := "2025-10-30")]

def Std.PRange.Nat.size_Rcc {a b : Nat} : (a...=b).size = b + 1 - a

Equations

• @Std.PRange.Nat.size_Rcc = @Std.PRange.Nat.size_rcc

@[simp]

theorem Std.PRange.Nat.size_rco {a b : Nat} : (a...b).size = b - a

@[deprecated Std.PRange.Nat.size_rco (since := "2025-10-30")]

def Std.PRange.Nat.size_Rco {a b : Nat} : (a...b).size = b - a

Equations

• @Std.PRange.Nat.size_Rco = @Std.PRange.Nat.size_rco

@[simp]

theorem Std.PRange.Nat.size_roc {a b : Nat} : (a<...=b).size = b - a

@[deprecated Std.PRange.Nat.size_roc (since := "2025-10-30")]

def Std.PRange.Nat.size_Roc {a b : Nat} : (a<...=b).size = b - a

Equations

• @Std.PRange.Nat.size_Roc = @Std.PRange.Nat.size_roc

@[simp]

theorem Std.PRange.Nat.size_roo {a b : Nat} : (a<...b).size = b - a - 1

@[deprecated Std.PRange.Nat.size_roo (since := "2025-10-30")]

def Std.PRange.Nat.size_Roo {a b : Nat} : (a<...b).size = b - a - 1

Equations

• @Std.PRange.Nat.size_Roo = @Std.PRange.Nat.size_roo

@[simp]

theorem Std.PRange.Nat.size_ric {b : Nat} : (*...=b).size = b + 1

@[deprecated Std.PRange.Nat.size_ric (since := "2025-10-30")]

def Std.PRange.Nat.size_Ric {b : Nat} : (*...=b).size = b + 1

Equations

• @Std.PRange.Nat.size_Ric = @Std.PRange.Nat.size_ric

@[simp]

theorem Std.PRange.Nat.size_rio {b : Nat} : (*...b).size = b

@[deprecated Std.PRange.Nat.size_rio (since := "2025-10-30")]

def Std.PRange.Nat.size_Rio {b : Nat} : (*...b).size = b

Equations

• @Std.PRange.Nat.size_Rio = @Std.PRange.Nat.size_rio