@[simp]

theorem Std.PRange.Nat.succ?_eq {n : Nat} : succ? n = some (n + 1)

@[simp]

theorem Std.PRange.Nat.succMany?_eq {m n : Nat} : succMany? n m = some (m + n)

@[simp]

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

@[simp]

theorem Std.PRange.Nat.succMany_eq {m n : Nat} : succMany n m = m + n

@[simp]

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

@[deprecated 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 = @Nat.size_rcc

@[deprecated Nat.size_rcc (since := "2025-12-01")]

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

Equations

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

@[simp]

theorem Nat.length_toList_rcc {a b : Nat} : (a...=b).toList.length = b + 1 - a

@[simp]

theorem Nat.size_toArray_rcc {a b : Nat} : (a...=b).toArray.size = b + 1 - a

@[simp]

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

@[deprecated 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 = @Nat.size_rco

@[deprecated Nat.size_rco (since := "2025-12-01")]

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

Equations

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

@[simp]

theorem Nat.length_toList_rco {a b : Nat} : (a...b).toList.length = b - a

@[simp]

theorem Nat.size_toArray_rco {a b : Nat} : (a...b).toArray.size = b - a

@[simp]

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

@[deprecated 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 = @Nat.size_roc

@[deprecated Nat.size_roc (since := "2025-12-01")]

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

Equations

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

@[simp]

theorem Nat.length_toList_roc {a b : Nat} : (a<...=b).toList.length = b - a

@[simp]

theorem Nat.size_toArray_roc {a b : Nat} : (a<...=b).toArray.size = b - a

@[simp]

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

@[deprecated 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 = @Nat.size_roo

@[deprecated Nat.size_roo (since := "2025-12-01")]

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

Equations

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

@[simp]

theorem Nat.length_toList_roo {a b : Nat} : (a<...b).toList.length = b - a - 1

@[simp]

theorem Nat.size_toArray_roo {a b : Nat} : (a<...b).toArray.size = b - a - 1

@[simp]

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

@[deprecated 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 = @Nat.size_ric

@[deprecated Nat.size_ric (since := "2025-12-01")]

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

Equations

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

@[simp]

theorem Nat.length_toList_ric {b : Nat} : (*...=b).toList.length = b + 1

@[simp]

theorem Nat.size_toArray_ric {b : Nat} : (*...=b).toArray.size = b + 1

@[simp]

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

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

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

Equations

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

@[deprecated Nat.size_rio (since := "2025-12-01")]

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

Equations

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

@[simp]

theorem Nat.length_toList_rio {b : Nat} : (*...b).toList.length = b

@[simp]

theorem Nat.size_toArray_rio {b : Nat} : (*...b).toArray.size = b

@[simp]

theorem Nat.toList_toArray_rco {m n : Nat} : (m...n).toArray.toList = (m...n).toList

@[simp]

theorem Nat.toArray_toList_rco {m n : Nat} : (m...n).toList.toArray = (m...n).toArray

theorem Nat.toList_rco_eq_if {m n : Nat} : (m...n).toList = if m < n then m :: ((m + 1)...n).toList else []

theorem Nat.toList_rco_succ_succ {m n : Nat} : ((m + 1)...n + 1).toList = List.map (fun (x : Nat) => x + 1) (m...n).toList

@[deprecated 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 = @Nat.toList_rco_succ_succ

@[deprecated Nat.toList_rco_succ_succ (since := "2025-12-01")]

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 = @Nat.toList_rco_succ_succ

theorem Nat.toList_rco_succ_right_eq_cons_map {m n : Nat} (h : m ≤ n) : (m...n + 1).toList = m :: List.map (fun (x : Nat) => x + 1) (m...n).toList

@[simp]

theorem Nat.toList_rco_eq_nil_iff {m n : Nat} : (m...n).toList = [] ↔ n ≤ m

theorem Nat.toList_rco_ne_nil_iff {m n : Nat} : (m...n).toList ≠ [] ↔ m < n

@[simp]

theorem Nat.toList_rco_eq_nil {m n : Nat} (h : n ≤ m) : (m...n).toList = []

@[simp]

theorem Nat.toList_rco_eq_singleton_iff {k m n : Nat} : (m...n).toList = [k] ↔ n = m + 1 ∧ m = k

@[simp]

theorem Nat.toList_rco_eq_singleton {m n : Nat} (h : n = m + 1) : (m...n).toList = [m]

@[simp]

theorem Nat.toList_rco_eq_cons_iff {xs : List Nat} {m n a : Nat} : (m...n).toList = a :: xs ↔ m = a ∧ m < n ∧ ((m + 1)...n).toList = xs

theorem Nat.toList_rco_eq_cons {m n : Nat} (h : m < n) : (m...n).toList = m :: ((m + 1)...n).toList

@[simp]

theorem Nat.toList_rco_zero_right_eq_nil {m : Nat} : (m...0).toList = []

theorem Nat.map_add_toList_rco {m n k : Nat} : List.map (fun (x : Nat) => x + k) (m...n).toList = ((m + k)...n + k).toList

theorem Nat.map_add_toList_rco' {m n k : Nat} : List.map (fun (x : Nat) => k + x) (m...n).toList = ((k + m)...k + n).toList

theorem Nat.toList_rco_add_right_eq_map {m n : Nat} : (m...m + n).toList = List.map (fun (x : Nat) => x + m) (0...n).toList

theorem Nat.toList_rco_add_succ_right_eq_append {m n : Nat} : (m...m + n + 1).toList = (m...m + n).toList ++ [m + n]

theorem Nat.toList_rco_succ_right_eq_append {m n : Nat} (h : m ≤ n) : (m...n + 1).toList = (m...n).toList ++ [n]

theorem Nat.toList_rco_add_succ_right_eq_append' {m n : Nat} : (m...m + (n + 1)).toList = (m...m + n).toList ++ [m + n]

theorem Nat.toList_rco_eq_append {m n : Nat} (h : m < n) : (m...n).toList = (m...n - 1).toList ++ [n - 1]

theorem Nat.toList_rco_eq_if_append {m n : Nat} : (m...n).toList = if m < n then (m...n - 1).toList ++ [n - 1] else []

theorem Nat.toList_rco_add_add_eq_append {m n k : Nat} : (m...m + n + k).toList = (m...m + n).toList ++ ((m + n)...m + n + k).toList

theorem Nat.toList_rco_append_toList_rco {l m n : Nat} (h : l ≤ m) (h' : m ≤ n) : (l...m).toList ++ (m...n).toList = (l...n).toList

@[simp]

theorem Nat.getElem_toList_rco {m n i : Nat} (_h : i < (m...n).toList.length) : (m...n).toList[i] = m + i

theorem Nat.getElem?_toList_rco {m n i : Nat} : (m...n).toList[i]? = if i < n - m then some (m + i) else none

@[simp]

theorem Nat.getElem?_toList_rco_eq_some_iff {k m n i : Nat} : (m...n).toList[i]? = some k ↔ i < n - m ∧ m + i = k

@[simp]

theorem Nat.getElem?_toList_rco_eq_none_iff {m n i : Nat} : (m...n).toList[i]? = none ↔ n ≤ i + m

@[simp]

theorem Nat.isSome_getElem?_toList_rco_eq {m n i : Nat} : ((m...n).toList[i]?.isSome = true) = (i < n - m)

@[simp]

theorem Nat.isNone_getElem?_toList_rco_eq {m n i : Nat} : ((m...n).toList[i]?.isNone = true) = (n ≤ i + m)

@[simp]

theorem Nat.getElem?_toList_rco_eq_some {m n i : Nat} (h : i < n - m) : (m...n).toList[i]? = some (m + i)

@[simp]

theorem Nat.getElem?_toList_rco_eq_none {m n i : Nat} (h : n ≤ i + m) : (m...n).toList[i]? = none

theorem Nat.getElem!_toList_rco {m n i : Nat} : (m...n).toList[i]! = if i < n - m then m + i else 0

@[simp]

theorem Nat.getElem!_toList_rco_eq_add {m n i : Nat} (h : i < n - m) : (m...n).toList[i]! = m + i

@[simp]

theorem Nat.getElem!_toList_rco_eq_zero {m n i : Nat} (h : n ≤ i + m) : (m...n).toList[i]! = 0

theorem Nat.getElem!_toList_rco_eq_zero_iff {m n i : Nat} : (m...n).toList[i]! = 0 ↔ n ≤ i + m ∨ m = 0 ∧ i = 0

theorem Nat.zero_lt_getElem!_toList_rco_iff {m n i : Nat} : 0 < (m...n).toList[i]! ↔ i < n - m ∧ 0 < i + m

theorem Nat.getD_toList_rco {m n i fallback : Nat} : (m...n).toList.getD i fallback = if i < n - m then m + i else fallback

@[simp]

theorem Nat.getD_toList_rco_eq_add {m n i fallback : Nat} (h : i < n - m) : (m...n).toList.getD i fallback = m + i

@[simp]

theorem Nat.getD_toList_rco_eq_fallback {m n i fallback : Nat} (h : n ≤ i + m) : (m...n).toList.getD i fallback = fallback

theorem Nat.toArray_rco_eq_if {m n : Nat} : (m...n).toArray = if m < n then #[m] ++ ((m + 1)...n).toArray else #[]

theorem Nat.toArray_rco_succ_succ {m n : Nat} : ((m + 1)...n + 1).toArray = Array.map (fun (x : Nat) => x + 1) (m...n).toArray

theorem Nat.toArray_rco_succ_right_eq_append_map {m n : Nat} (h : m ≤ n) : (m...n + 1).toArray = #[m] ++ Array.map (fun (x : Nat) => x + 1) (m...n).toArray

@[simp]

theorem Nat.toArray_rco_eq_empty_iff {m n : Nat} : (m...n).toArray = #[] ↔ n ≤ m

theorem Nat.toArray_rco_ne_empty_iff {m n : Nat} : (m...n).toArray ≠ #[] ↔ m < n

@[simp]

theorem Nat.toArray_rco_eq_empty {m n : Nat} (h : n ≤ m) : (m...n).toArray = #[]

@[simp]

theorem Nat.toArray_rco_eq_singleton_iff {k m n : Nat} : (m...n).toArray = #[k] ↔ n = m + 1 ∧ m = k

@[simp]

theorem Nat.toArray_rco_eq_singleton {m n : Nat} (h : n = m + 1) : (m...n).toArray = #[m]

@[simp]

theorem Nat.toArray_rco_eq_singleton_append_iff {xs : Array Nat} {m n a : Nat} : (m...n).toArray = #[a] ++ xs ↔ m = a ∧ m < n ∧ ((m + 1)...n).toArray = xs

theorem Nat.toArray_rco_eq_singleton_append {m n : Nat} (h : m < n) : (m...n).toArray = #[m] ++ ((m + 1)...n).toArray

@[simp]

theorem Nat.toArray_rco_zero_right_eq_empty {m : Nat} : (m...0).toArray = #[]

theorem Nat.map_add_toArray_rco {m n k : Nat} : Array.map (fun (x : Nat) => x + k) (m...n).toArray = ((m + k)...n + k).toArray

theorem Nat.map_add_toArray_rco' {m n k : Nat} : Array.map (fun (x : Nat) => k + x) (m...n).toArray = ((k + m)...k + n).toArray

theorem Nat.toArray_rco_add_right_eq_map {m n : Nat} : (m...m + n).toArray = Array.map (fun (x : Nat) => x + m) (0...n).toArray

theorem Nat.toArray_rco_add_succ_right_eq_push {m n : Nat} : (m...m + n + 1).toArray = (m...m + n).toArray.push (m + n)

theorem Nat.toArray_rco_succ_right_eq_push {m n : Nat} (h : m ≤ n) : (m...n + 1).toArray = (m...n).toArray.push n

theorem Nat.toArray_rco_add_succ_right_eq_push' {m n : Nat} : (m...m + (n + 1)).toArray = (m...m + n).toArray.push (m + n)

theorem Nat.toArray_rco_eq_push {m n : Nat} (h : m < n) : (m...n).toArray = (m...n - 1).toArray.push (n - 1)

theorem Nat.toArray_rco_eq_if_push {m n : Nat} : (m...n).toArray = if m < n then (m...n - 1).toArray.push (n - 1) else #[]

theorem Nat.toArray_rco_add_add_eq_append {m n k : Nat} : (m...m + n + k).toArray = (m...m + n).toArray ++ ((m + n)...m + n + k).toArray

theorem Nat.toArray_rco_append_toArray_rco {l m n : Nat} (h : l ≤ m) (h' : m ≤ n) : (l...m).toArray ++ (m...n).toArray = (l...n).toArray

@[simp]

theorem Nat.getElem_toArray_rco {m n i : Nat} (_h : i < (m...n).toArray.size) : (m...n).toArray[i] = m + i

theorem Nat.getElem?_toArray_rco {m n i : Nat} : (m...n).toArray[i]? = if i < n - m then some (m + i) else none

@[simp]

theorem Nat.getElem?_toArray_rco_eq_some_iff {k m n i : Nat} : (m...n).toArray[i]? = some k ↔ i < n - m ∧ m + i = k

@[simp]

theorem Nat.getElem?_toArray_rco_eq_none_iff {m n i : Nat} : (m...n).toArray[i]? = none ↔ n ≤ i + m

@[simp]

theorem Nat.isSome_getElem?_toArray_rco_eq {m n i : Nat} : ((m...n).toArray[i]?.isSome = true) = (i < n - m)

@[simp]

theorem Nat.isNone_getElem?_toArray_rco_eq {m n i : Nat} : ((m...n).toArray[i]?.isNone = true) = (n ≤ i + m)

@[simp]

theorem Nat.getElem?_toArray_rco_eq_some {m n i : Nat} (h : i < n - m) : (m...n).toArray[i]? = some (m + i)

@[simp]

theorem Nat.getElem?_toArray_rco_eq_none {m n i : Nat} (h : n ≤ i + m) : (m...n).toArray[i]? = none

theorem Nat.getElem!_toArray_rco {m n i : Nat} : (m...n).toArray[i]! = if i < n - m then m + i else 0

@[simp]

theorem Nat.getElem!_toArray_rco_eq_add {m n i : Nat} (h : i < n - m) : (m...n).toArray[i]! = m + i

@[simp]

theorem Nat.getElem!_toArray_rco_eq_zero {m n i : Nat} (h : n ≤ i + m) : (m...n).toArray[i]! = 0

theorem Nat.getElem!_toArray_rco_eq_zero_iff {m n i : Nat} : (m...n).toArray[i]! = 0 ↔ n ≤ i + m ∨ m = 0 ∧ i = 0

theorem Nat.zero_lt_getElem!_toArray_rco_iff {m n i : Nat} : 0 < (m...n).toArray[i]! ↔ i < n - m ∧ 0 < i + m

theorem Nat.getD_toArray_rco {m n i fallback : Nat} : (m...n).toArray.getD i fallback = if i < n - m then m + i else fallback

@[simp]

theorem Nat.getD_toArray_rco_eq_add {m n i fallback : Nat} (h : i < n - m) : (m...n).toArray.getD i fallback = m + i

@[simp]

theorem Nat.getD_toArray_rco_eq_fallback {m n i fallback : Nat} (h : n ≤ i + m) : (m...n).toArray.getD i fallback = fallback

theorem Nat.induct_rco_left (motive : Nat → Nat → Prop) (base : ∀ (a b : Nat), b ≤ a → motive a b) (step : ∀ (a b : Nat), a < b → motive (a + 1) b → motive a b) (a b : Nat) : motive a b

Induction principle for proving properties of Nat-based ranges of the form a...b by varying the lower bound.

In the base case, one proves that for any a : Nat and b : Nat with b ≤ a, the statement holds for the empty range a...b.

In the step case, one proves that for any a : Nat and b : Nat, the statement holds for nonempty ranges a...b if it holds for the smaller range (a + 1)...b.

The following is an example reproving length_toList_rco.

example (a b : Nat) : (a...b).toList.length = b - a := by
  induction a, b using Nat.induct_rco_left
  case base =>
    simp only [Nat.toList_rco_eq_nil, List.length_nil, Nat.sub_eq_zero_of_le, *]
  case step =>
    simp only [Nat.toList_rco_eq_cons, List.length_cons, *]; omega

theorem Nat.induct_rco_right (motive : Nat → Nat → Prop) (base : ∀ (a b : Nat), b ≤ a → motive a b) (step : ∀ (a b : Nat), a ≤ b → motive a b → motive a (b + 1)) (a b : Nat) : motive a b

Induction principle for proving properties of Nat-based ranges of the form a...b by varying the upper bound.

In the base case, one proves that for any a : Nat and b : Nat with b ≤ a, the statement holds for the empty range a...b.

In the step case, one proves that for any a : Nat and b : Nat, if the statement holds for a...b, it also holds for the larger range a...(b + 1).

The following is an example reproving length_toList_rco.

example (a b : Nat) : (a...b).toList.length = b - a := by
  induction a, b using Nat.induct_rco_right
  case base =>
    simp only [Nat.toList_rco_eq_nil, List.length_nil, Nat.sub_eq_zero_of_le, *]
  case step a b hle ih =>
    rw [Nat.toList_rco_eq_append (by omega),
      List.length_append, List.length_singleton, Nat.add_sub_cancel, ih]
    omega

@[simp]

theorem Nat.toList_rcc_eq_toList_rco {m n : Nat} : (m...=n).toList = (m...n + 1).toList

@[simp]

theorem Nat.toList_toArray_rcc {m n : Nat} : (m...=n).toArray.toList = (m...=n).toList

@[simp]

theorem Nat.toArray_toList_rcc {m n : Nat} : (m...=n).toList.toArray = (m...=n).toArray

theorem Nat.toList_rcc_eq_if {m n : Nat} : (m...=n).toList = if m ≤ n then m :: ((m + 1)...=n).toList else []

theorem Nat.toList_rcc_succ_succ {m n : Nat} : ((m + 1)...=n + 1).toList = List.map (fun (x : Nat) => x + 1) (m...=n).toList

theorem Nat.toList_rcc_succ_right_eq_cons_map {m n : Nat} (h : m ≤ n + 1) : (m...=n + 1).toList = m :: List.map (fun (x : Nat) => x + 1) (m...=n).toList

@[simp]

theorem Nat.toList_rcc_eq_nil_iff {m n : Nat} : (m...=n).toList = [] ↔ n < m

theorem Nat.toList_rcc_ne_nil_iff {m n : Nat} : (m...=n).toList ≠ [] ↔ m ≤ n

@[simp]

theorem Nat.toList_rcc_eq_nil {m n : Nat} (h : n < m) : (m...=n).toList = []

@[simp]

theorem Nat.toList_rcc_eq_singleton_iff {k m n : Nat} : (m...=n).toList = [k] ↔ n = m ∧ m = k

@[simp]

theorem Nat.toList_rcc_eq_singleton {m n : Nat} (h : n = m) : (m...=n).toList = [m]

@[simp]

theorem Nat.toList_rcc_eq_cons_iff {xs : List Nat} {m n a : Nat} : (m...=n).toList = a :: xs ↔ m = a ∧ m ≤ n ∧ ((m + 1)...=n).toList = xs

theorem Nat.toList_rcc_eq_cons {m n : Nat} (h : m ≤ n) : (m...=n).toList = m :: ((m + 1)...=n).toList

theorem Nat.map_add_toList_rcc {m n k : Nat} : List.map (fun (x : Nat) => x + k) (m...=n).toList = ((m + k)...=n + k).toList

theorem Nat.map_add_toList_rcc' {m n k : Nat} : List.map (fun (x : Nat) => k + x) (m...=n).toList = ((k + m)...=k + n).toList

theorem Nat.toList_rcc_add_right_eq_map {m n : Nat} : (m...=m + n).toList = List.map (fun (x : Nat) => x + m) (0...=n).toList

theorem Nat.toList_rcc_add_succ_right_eq_append {m n : Nat} : (m...=m + n + 1).toList = (m...=m + n).toList ++ [m + n + 1]

@[simp]

theorem Nat.toList_rcc_eq_append {m n : Nat} (h : m ≤ n) : (m...=n).toList = (m...n).toList ++ [n]

theorem Nat.toList_rcc_succ_right_eq_append {m n : Nat} (h : m ≤ n + 1) : (m...=n + 1).toList = (m...=n).toList ++ [n + 1]

theorem Nat.toList_rcc_add_succ_right_eq_append' {m n : Nat} : (m...=m + (n + 1)).toList = (m...=m + n).toList ++ [m + n + 1]

@[simp]

theorem Nat.getElem_toList_rcc {m n i : Nat} (_h : i < (m...=n).toList.length) : (m...=n).toList[i] = m + i

theorem Nat.getElem?_toList_rcc {m n i : Nat} : (m...=n).toList[i]? = if i < n + 1 - m then some (m + i) else none

@[simp]

theorem Nat.getElem?_toList_rcc_eq_some_iff {k m n i : Nat} : (m...=n).toList[i]? = some k ↔ i < n + 1 - m ∧ m + i = k

@[simp]

theorem Nat.getElem?_toList_rcc_eq_none_iff {m n i : Nat} : (m...=n).toList[i]? = none ↔ n + 1 ≤ i + m

@[simp]

theorem Nat.isSome_getElem?_toList_rcc_eq {m n i : Nat} : ((m...=n).toList[i]?.isSome = true) = (i < n + 1 - m)

@[simp]

theorem Nat.isNone_getElem?_toList_rcc_eq {m n i : Nat} : ((m...=n).toList[i]?.isNone = true) = (n + 1 ≤ i + m)

@[simp]

theorem Nat.getElem?_toList_rcc_eq_some {m n i : Nat} (h : i < n + 1 - m) : (m...=n).toList[i]? = some (m + i)

@[simp]

theorem Nat.getElem?_toList_rcc_eq_none {m n i : Nat} (h : n + 1 ≤ i + m) : (m...=n).toList[i]? = none

theorem Nat.getElem!_toList_rcc {m n i : Nat} : (m...=n).toList[i]! = if i < n + 1 - m then m + i else 0

@[simp]

theorem Nat.getElem!_toList_rcc_eq_add {m n i : Nat} (h : i < n + 1 - m) : (m...=n).toList[i]! = m + i

@[simp]

theorem Nat.getElem!_toList_rcc_eq_zero {m n i : Nat} (h : n + 1 ≤ i + m) : (m...=n).toList[i]! = 0

theorem Nat.getElem!_toList_rcc_eq_zero_iff {m n i : Nat} : (m...=n).toList[i]! = 0 ↔ n + 1 ≤ i + m ∨ m = 0 ∧ i = 0

theorem Nat.zero_lt_getElem!_toList_rcc_iff {m n i : Nat} : 0 < (m...=n).toList[i]! ↔ i < n + 1 - m ∧ 0 < i + m

theorem Nat.getD_toList_rcc {m n i fallback : Nat} : (m...=n).toList.getD i fallback = if i < n + 1 - m then m + i else fallback

@[simp]

theorem Nat.getD_toList_rcc_eq_add {m n i fallback : Nat} (h : i < n + 1 - m) : (m...=n).toList.getD i fallback = m + i

@[simp]

theorem Nat.getD_toList_rcc_eq_fallback {m n i fallback : Nat} (h : n + 1 ≤ i + m) : (m...=n).toList.getD i fallback = fallback

@[simp]

theorem Nat.toArray_rcc_eq_toArray_rco {m n : Nat} : (m...=n).toArray = (m...n + 1).toArray

theorem Nat.toArray_rcc_eq_if {m n : Nat} : (m...=n).toArray = if m ≤ n then #[m] ++ ((m + 1)...=n).toArray else #[]

theorem Nat.toArray_rcc_succ_succ {m n : Nat} : ((m + 1)...=n + 1).toArray = Array.map (fun (x : Nat) => x + 1) (m...=n).toArray

theorem Nat.toArray_rcc_succ_right_eq_append_map {m n : Nat} (h : m ≤ n + 1) : (m...=n + 1).toArray = #[m] ++ Array.map (fun (x : Nat) => x + 1) (m...=n).toArray

@[simp]

theorem Nat.toArray_rcc_eq_empty_iff {m n : Nat} : (m...=n).toArray = #[] ↔ n < m

theorem Nat.toArray_rcc_ne_empty_iff {m n : Nat} : (m...=n).toArray ≠ #[] ↔ m ≤ n

@[simp]

theorem Nat.toArray_rcc_eq_empty {m n : Nat} (h : n < m) : (m...=n).toArray = #[]

@[simp]

theorem Nat.toArray_rcc_eq_singleton_iff {k m n : Nat} : (m...=n).toArray = #[k] ↔ n = m ∧ m = k

@[simp]

theorem Nat.toArray_rcc_eq_singleton {m n : Nat} (h : n = m) : (m...=n).toArray = #[m]

@[simp]

theorem Nat.toArray_rcc_eq_singleton_append_iff {xs : Array Nat} {m n a : Nat} : (m...=n).toArray = #[a] ++ xs ↔ m = a ∧ m ≤ n ∧ ((m + 1)...=n).toArray = xs

theorem Nat.toArray_rcc_eq_singleton_append {m n : Nat} (h : m ≤ n) : (m...=n).toArray = #[m] ++ ((m + 1)...=n).toArray

theorem Nat.map_add_toArray_rcc {m n k : Nat} : Array.map (fun (x : Nat) => x + k) (m...=n).toArray = ((m + k)...=n + k).toArray

theorem Nat.map_add_toArray_rcc' {m n k : Nat} : Array.map (fun (x : Nat) => k + x) (m...=n).toArray = ((k + m)...=k + n).toArray

theorem Nat.toArray_rcc_add_right_eq_map {m n : Nat} : (m...=m + n).toArray = Array.map (fun (x : Nat) => x + m) (0...=n).toArray

theorem Nat.toArray_rcc_add_succ_right_eq_push {m n : Nat} : (m...=m + n + 1).toArray = (m...=m + n).toArray.push (m + n + 1)

@[simp]

theorem Nat.toArray_rcc_eq_push {m n : Nat} (h : m ≤ n) : (m...=n).toArray = (m...n).toArray.push n

theorem Nat.toArray_rcc_succ_right_eq_push {m n : Nat} (h : m ≤ n + 1) : (m...=n + 1).toArray = (m...=n).toArray.push (n + 1)

theorem Nat.toArray_rcc_add_succ_right_eq_push' {m n : Nat} : (m...=m + (n + 1)).toArray = (m...=m + n).toArray.push (m + n + 1)

@[simp]

theorem Nat.getElem_toArray_rcc {m n i : Nat} (_h : i < (m...=n).toArray.size) : (m...=n).toArray[i] = m + i

theorem Nat.getElem?_toArray_rcc {m n i : Nat} : (m...=n).toArray[i]? = if i < n + 1 - m then some (m + i) else none

@[simp]

theorem Nat.getElem?_toArray_rcc_eq_some_iff {k m n i : Nat} : (m...=n).toArray[i]? = some k ↔ i < n + 1 - m ∧ m + i = k

@[simp]

theorem Nat.getElem?_toArray_rcc_eq_none_iff {m n i : Nat} : (m...=n).toArray[i]? = none ↔ n + 1 ≤ i + m

@[simp]

theorem Nat.isSome_getElem?_toArray_rcc_eq {m n i : Nat} : ((m...=n).toArray[i]?.isSome = true) = (i < n + 1 - m)

@[simp]

theorem Nat.isNone_getElem?_toArray_rcc_eq {m n i : Nat} : ((m...=n).toArray[i]?.isNone = true) = (n + 1 ≤ i + m)

@[simp]

theorem Nat.getElem?_toArray_rcc_eq_some {m n i : Nat} (h : i < n + 1 - m) : (m...=n).toArray[i]? = some (m + i)

@[simp]

theorem Nat.getElem?_toArray_rcc_eq_none {m n i : Nat} (h : n + 1 ≤ i + m) : (m...=n).toArray[i]? = none

theorem Nat.getElem!_toArray_rcc {m n i : Nat} : (m...=n).toArray[i]! = if i < n + 1 - m then m + i else 0

@[simp]

theorem Nat.getElem!_toArray_rcc_eq_add {m n i : Nat} (h : i < n + 1 - m) : (m...=n).toArray[i]! = m + i

@[simp]

theorem Nat.getElem!_toArray_rcc_eq_zero {m n i : Nat} (h : n + 1 ≤ i + m) : (m...=n).toArray[i]! = 0

theorem Nat.getElem!_toArray_rcc_eq_zero_iff {m n i : Nat} : (m...=n).toArray[i]! = 0 ↔ n + 1 ≤ i + m ∨ m = 0 ∧ i = 0

theorem Nat.zero_lt_getElem!_toArray_rcc_iff {m n i : Nat} : 0 < (m...=n).toArray[i]! ↔ i < n + 1 - m ∧ 0 < i + m

theorem Nat.getD_toArray_rcc {m n i fallback : Nat} : (m...=n).toArray.getD i fallback = if i < n + 1 - m then m + i else fallback

@[simp]

theorem Nat.getD_toArray_rcc_eq_add {m n i fallback : Nat} (h : i < n + 1 - m) : (m...=n).toArray.getD i fallback = m + i

@[simp]

theorem Nat.getD_toArray_rcc_eq_fallback {m n i fallback : Nat} (h : n + 1 ≤ i + m) : (m...=n).toArray.getD i fallback = fallback

theorem Nat.induct_rcc_left (motive : Nat → Nat → Prop) (base : ∀ (a b : Nat), b < a → motive a b) (step : ∀ (a b : Nat), a ≤ b → motive (a + 1) b → motive a b) (a b : Nat) : motive a b

Induction principle for proving properties of Nat-based ranges of the form a...=b by varying the lower bound.

In the base case, one proves that for any a : Nat and b : Nat with b < a, the statement holds for the empty range a...=b.

In the step case, one proves that for any a : Nat and b : Nat, the statement holds for nonempty ranges a...b if it holds for the smaller range (a + 1)...=b.

The following is an example reproving length_toList_rcc.

example (a b : Nat) : (a...=b).toList.length = b + 1 - a := by
  induction a, b using Nat.induct_rcc_left
  case base =>
    simp only [Nat.toList_rcc_eq_nil, List.length_nil, *]; omega
  case step =>
    simp only [Nat.toList_rcc_eq_cons, List.length_cons, *]; omega

theorem Nat.induct_rcc_right (motive : Nat → Nat → Prop) (base : ∀ (a b : Nat), b ≤ a → motive a b) (step : ∀ (a b : Nat), a ≤ b → motive a b → motive a (b + 1)) (a b : Nat) : motive a b

Induction principle for proving properties of Nat-based ranges of the form a...=b by varying the upper bound.

In the base case, one proves that for any a : Nat and b : Nat with b ≤ a, the statement holds for the subsingleton range a...=b.

In the step case, one proves that for any a : Nat and b : Nat, if the statement holds for a...=b, it also holds for the larger range a...=(b + 1).

The following is an example reproving length_toList_rcc.

example (a b : Nat) : (a...=b).toList.length = b + 1 - a := by
  induction a, b using Nat.induct_rcc_right
  case base a b hge =>
    by_cases h : b < a
    · simp only [Nat.toList_rcc_eq_nil, List.length_nil, *]
      omega
    · have : b = a := by omega
      simp only [Nat.toList_rcc_eq_singleton, List.length_singleton,
        Nat.add_sub_cancel_left, *]
  case step a b hle ih =>
    rw [Nat.toList_rcc_succ_right_eq_append (by omega), List.length_append,
      List.length_singleton, ih] <;> omega

@[simp]

theorem Nat.toList_roo_eq_toList_rco {m n : Nat} : (m<...n).toList = ((m + 1)...n).toList

@[simp]

theorem Nat.toList_toArray_roo {m n : Nat} : (m<...n).toArray.toList = (m<...n).toList

@[simp]

theorem Nat.toArray_toList_roo {m n : Nat} : (m<...n).toList.toArray = (m<...n).toArray

theorem Nat.toList_roo_eq_if {m n : Nat} : (m<...n).toList = if m + 1 < n then (m + 1) :: ((m + 1)<...n).toList else []

theorem Nat.toList_roo_succ_succ {m n : Nat} : ((m + 1)<...n + 1).toList = List.map (fun (x : Nat) => x + 1) (m<...n).toList

theorem Nat.toList_roo_succ_right_eq_cons_map {m n : Nat} (h : m < n) : (m<...n + 1).toList = (m + 1) :: List.map (fun (x : Nat) => x + 1) (m<...n).toList

@[simp]

theorem Nat.toList_roo_eq_nil_iff {m n : Nat} : (m<...n).toList = [] ↔ n ≤ m + 1

theorem Nat.toList_roo_ne_nil_iff {m n : Nat} : (m<...n).toList ≠ [] ↔ m + 1 < n

@[simp]

theorem Nat.toList_roo_eq_nil {m n : Nat} (h : n ≤ m + 1) : (m<...n).toList = []

@[simp]

theorem Nat.toList_roo_eq_singleton_iff {k m n : Nat} : (m<...n).toList = [k] ↔ n = m + 2 ∧ m + 1 = k

@[simp]

theorem Nat.toList_roo_eq_singleton {m n : Nat} (h : n = m + 2) : (m<...n).toList = [m + 1]

@[simp]

theorem Nat.toList_roo_eq_cons_iff {xs : List Nat} {m n a : Nat} : (m<...n).toList = a :: xs ↔ m + 1 = a ∧ m + 1 < n ∧ ((m + 1)<...n).toList = xs

theorem Nat.toList_roo_eq_cons {m n : Nat} (h : m + 1 < n) : (m<...n).toList = (m + 1) :: ((m + 1)<...n).toList

@[simp]

theorem Nat.toList_roo_zero_right_eq_nil {m : Nat} : (m<...0).toList = []

@[simp]

theorem Nat.toList_roo_one_right_eq_nil {m : Nat} : (m<...1).toList = []

theorem Nat.map_add_toList_roo {m n k : Nat} : List.map (fun (x : Nat) => x + k) (m<...n).toList = ((m + k)<...n + k).toList

theorem Nat.map_add_toList_roo' {m n k : Nat} : List.map (fun (x : Nat) => k + x) (m<...n).toList = ((k + m)<...k + n).toList

theorem Nat.toList_roo_add_right_eq_map {m n : Nat} : (m<...m + 1 + n).toList = List.map (fun (x : Nat) => x + m + 1) (0...n).toList

theorem Nat.toList_roo_succ_right_eq_append {m n : Nat} (h : m < n) : (m<...n + 1).toList = (m<...n).toList ++ [n]

@[simp]

theorem Nat.toList_roo_eq_append {m n : Nat} (h : m + 1 < n) : (m<...n).toList = (m<...n - 1).toList ++ [n - 1]

@[simp]

theorem Nat.getElem_toList_roo {m n i : Nat} (_h : i < (m<...n).toList.length) : (m<...n).toList[i] = m + 1 + i

theorem Nat.getElem?_toList_roo {m n i : Nat} : (m<...n).toList[i]? = if i < n - (m + 1) then some (m + 1 + i) else none

@[simp]

theorem Nat.getElem?_toList_roo_eq_some_iff {k m n i : Nat} : (m<...n).toList[i]? = some k ↔ i < n - (m + 1) ∧ m + 1 + i = k

@[simp]

theorem Nat.getElem?_toList_roo_eq_none_iff {m n i : Nat} : (m<...n).toList[i]? = none ↔ n ≤ i + (m + 1)

@[simp]

theorem Nat.isSome_getElem?_toList_roo_eq {m n i : Nat} : ((m<...n).toList[i]?.isSome = true) = (i < n - (m + 1))

@[simp]

theorem Nat.isNone_getElem?_toList_roo_eq {m n i : Nat} : ((m<...n).toList[i]?.isNone = true) = (n ≤ i + (m + 1))

@[simp]

theorem Nat.getElem?_toList_roo_eq_some {m n i : Nat} (h : i < n - (m + 1)) : (m<...n).toList[i]? = some (m + 1 + i)

@[simp]

theorem Nat.getElem?_toList_roo_eq_none {m n i : Nat} (h : n ≤ i + (m + 1)) : (m<...n).toList[i]? = none

theorem Nat.getElem!_toList_roo {m n i : Nat} : (m<...n).toList[i]! = if i < n - (m + 1) then m + 1 + i else 0

@[simp]

theorem Nat.getElem!_toList_roo_eq_add {m n i : Nat} (h : i < n - (m + 1)) : (m<...n).toList[i]! = m + 1 + i

@[simp]

theorem Nat.getElem!_toList_roo_eq_zero {m n i : Nat} (h : n ≤ i + (m + 1)) : (m<...n).toList[i]! = 0

theorem Nat.getElem!_toList_roo_eq_zero_iff {m n i : Nat} : (m<...n).toList[i]! = 0 ↔ n ≤ i + (m + 1)

theorem Nat.zero_lt_getElem!_toList_roo_iff {m n i : Nat} : 0 < (m<...n).toList[i]! ↔ i < n - (m + 1)

theorem Nat.getD_toList_roo {m n i fallback : Nat} : (m<...n).toList.getD i fallback = if i < n - (m + 1) then m + 1 + i else fallback

@[simp]

theorem Nat.getD_toList_roo_eq_add {m n i fallback : Nat} (h : i < n - (m + 1)) : (m<...n).toList.getD i fallback = m + 1 + i

@[simp]

theorem Nat.getD_toList_roo_eq_fallback {m n i fallback : Nat} (h : n ≤ i + (m + 1)) : (m<...n).toList.getD i fallback = fallback

@[simp]

theorem Nat.toArray_roo_eq_toArray_rco {m n : Nat} : (m<...n).toArray = ((m + 1)...n).toArray

theorem Nat.toArray_roo_eq_if {m n : Nat} : (m<...n).toArray = if m + 1 < n then #[m + 1] ++ ((m + 1)<...n).toArray else #[]

theorem Nat.toArray_roo_succ_succ {m n : Nat} : ((m + 1)<...n + 1).toArray = Array.map (fun (x : Nat) => x + 1) (m<...n).toArray

theorem Nat.toArray_roo_succ_right_eq_append_map {m n : Nat} (h : m < n) : (m<...n + 1).toArray = #[m + 1] ++ Array.map (fun (x : Nat) => x + 1) (m<...n).toArray

@[simp]

theorem Nat.toArray_roo_eq_nil_iff {m n : Nat} : (m<...n).toArray = #[] ↔ n ≤ m + 1

theorem Nat.toArray_roo_ne_nil_iff {m n : Nat} : (m<...n).toArray ≠ #[] ↔ m + 1 < n

@[simp]

theorem Nat.toArray_roo_eq_nil {m n : Nat} (h : n ≤ m + 1) : (m<...n).toArray = #[]

@[simp]

theorem Nat.toArray_roo_eq_singleton_iff {k m n : Nat} : (m<...n).toArray = #[k] ↔ n = m + 2 ∧ m + 1 = k

@[simp]

theorem Nat.toArray_roo_eq_singleton {m n : Nat} (h : n = m + 2) : (m<...n).toArray = #[m + 1]

@[simp]

theorem Nat.toArray_roo_eq_singleton_append_iff {xs : Array Nat} {m n a : Nat} : (m<...n).toArray = #[a] ++ xs ↔ m + 1 = a ∧ m + 1 < n ∧ ((m + 1)<...n).toArray = xs

theorem Nat.toArray_roo_eq_singleton_append {m n : Nat} (h : m + 1 < n) : (m<...n).toArray = #[m + 1] ++ ((m + 1)<...n).toArray

@[simp]

theorem Nat.toArray_roo_zero_right_eq_nil {m : Nat} : (m<...0).toArray = #[]

@[simp]

theorem Nat.toArray_roo_one_right_eq_nil {m : Nat} : (m<...1).toArray = #[]

theorem Nat.map_add_toArray_roo {m n k : Nat} : Array.map (fun (x : Nat) => x + k) (m<...n).toArray = ((m + k)<...n + k).toArray

theorem Nat.map_add_toArray_roo' {m n k : Nat} : Array.map (fun (x : Nat) => k + x) (m<...n).toArray = ((k + m)<...k + n).toArray

theorem Nat.toArray_roo_add_right_eq_map {m n : Nat} : (m<...m + 1 + n).toArray = Array.map (fun (x : Nat) => x + m + 1) (0...n).toArray

theorem Nat.toArray_roo_succ_right_eq_push {m n : Nat} (h : m < n) : (m<...n + 1).toArray = (m<...n).toArray.push n

@[simp]

theorem Nat.toArray_roo_eq_push {m n : Nat} (h : m + 1 < n) : (m<...n).toArray = (m<...n - 1).toArray.push (n - 1)

@[simp]

theorem Nat.getElem_toArray_roo {m n i : Nat} (_h : i < (m<...n).toArray.size) : (m<...n).toArray[i] = m + 1 + i

theorem Nat.getElem?_toArray_roo {m n i : Nat} : (m<...n).toArray[i]? = if i < n - (m + 1) then some (m + 1 + i) else none

@[simp]

theorem Nat.getElem?_toArray_roo_eq_some_iff {k m n i : Nat} : (m<...n).toArray[i]? = some k ↔ i < n - (m + 1) ∧ m + 1 + i = k

@[simp]

theorem Nat.getElem?_toArray_roo_eq_none_iff {m n i : Nat} : (m<...n).toArray[i]? = none ↔ n ≤ i + (m + 1)

@[simp]

theorem Nat.isSome_getElem?_toArray_roo_eq {m n i : Nat} : ((m<...n).toArray[i]?.isSome = true) = (i < n - (m + 1))

@[simp]

theorem Nat.isNone_getElem?_toArray_roo_eq {m n i : Nat} : ((m<...n).toArray[i]?.isNone = true) = (n ≤ i + (m + 1))

@[simp]

theorem Nat.getElem?_toArray_roo_eq_some {m n i : Nat} (h : i < n - (m + 1)) : (m<...n).toArray[i]? = some (m + 1 + i)

@[simp]

theorem Nat.getElem?_toArray_roo_eq_none {m n i : Nat} (h : n ≤ i + (m + 1)) : (m<...n).toArray[i]? = none

theorem Nat.getElem!_toArray_roo {m n i : Nat} : (m<...n).toArray[i]! = if i < n - (m + 1) then m + 1 + i else 0

@[simp]

theorem Nat.getElem!_toArray_roo_eq_add {m n i : Nat} (h : i < n - (m + 1)) : (m<...n).toArray[i]! = m + 1 + i

@[simp]

theorem Nat.getElem!_toArray_roo_eq_zero {m n i : Nat} (h : n ≤ i + (m + 1)) : (m<...n).toArray[i]! = 0

theorem Nat.getElem!_toArray_roo_eq_zero_iff {m n i : Nat} : (m<...n).toArray[i]! = 0 ↔ n ≤ i + (m + 1)

theorem Nat.zero_lt_getElem!_toArray_roo_iff {m n i : Nat} : 0 < (m<...n).toArray[i]! ↔ i < n - (m + 1)

theorem Nat.getD_toArray_roo {m n i fallback : Nat} : (m<...n).toArray.getD i fallback = if i < n - (m + 1) then m + 1 + i else fallback

@[simp]

theorem Nat.getD_toArray_roo_eq_add {m n i fallback : Nat} (h : i < n - (m + 1)) : (m<...n).toArray.getD i fallback = m + 1 + i

@[simp]

theorem Nat.getD_toArray_roo_eq_fallback {m n i fallback : Nat} (h : n ≤ i + (m + 1)) : (m<...n).toArray.getD i fallback = fallback

theorem Nat.induct_roo_left (motive : Nat → Nat → Prop) (base : ∀ (a b : Nat), b ≤ a + 1 → motive a b) (step : ∀ (a b : Nat), a + 1 < b → motive (a + 1) b → motive a b) (a b : Nat) : motive a b

Induction principle for proving properties of Nat-based ranges of the form a<...b by varying the lower bound.

In the base case, one proves that for any a : Nat and b : Nat with b ≤ a + 1, the statement holds for the empty range a<...b.

In the step case, one proves that for any a : Nat and b : Nat, the statement holds for nonempty ranges a<...b if it holds for the smaller range (a + 1)<...b.

The following is an example reproving length_toList_roo.

example (a b : Nat) : (a<...b).toList.length = b - a - 1 := by
  induction a, b using Nat.induct_roo_left
  case base =>
    simp only [Nat.toList_roo_eq_nil, List.length_nil, *]; omega
  case step =>
    simp only [Nat.toList_roo_eq_cons, List.length_cons, *]; omega

theorem Nat.induct_roo_right (motive : Nat → Nat → Prop) (base : ∀ (a b : Nat), b ≤ a + 1 → motive a b) (step : ∀ (a b : Nat), a + 1 ≤ b → motive a b → motive a (b + 1)) (a b : Nat) : motive a b

Induction principle for proving properties of Nat-based ranges of the form a<...b by varying the upper bound.

In the base case, one proves that for any a : Nat and b : Nat with b ≤ a + 1, the statement holds for the empty range a<...b.

In the step case, one proves that for any a : Nat and b : Nat, if the statement holds for a<...b, it also holds for the larger range a<...(b + 1).

The following is an example reproving length_toList_roo.

example (a b : Nat) : (a<...b).toList.length = b - a - 1 := by
  induction a, b using Nat.induct_roo_right
  case base =>
    simp only [Nat.toList_roo_eq_nil, List.length_nil, *]; omega
  case step a b hle ih =>
    rw [Nat.toList_roo_eq_append (by omega),
      List.length_append, List.length_singleton, Nat.add_sub_cancel, ih]
    omega

theorem Nat.toList_roc_eq_toList_rcc {m n : Nat} : (m<...=n).toList = ((m + 1)...=n).toList

theorem Nat.toList_roc_eq_toList_roo {m n : Nat} : (m<...=n).toList = (m<...n + 1).toList

theorem Nat.toList_roc_eq_toList_rco {m n : Nat} : (m<...=n).toList = ((m + 1)...n + 1).toList

@[simp]

theorem Nat.toList_toArray_roc {m n : Nat} : (m<...=n).toArray.toList = (m<...=n).toList

@[simp]

theorem Nat.toArray_toList_roc {m n : Nat} : (m<...=n).toList.toArray = (m<...=n).toArray

theorem Nat.toList_roc_eq_if {m n : Nat} : (m<...=n).toList = if m + 1 ≤ n then (m + 1) :: ((m + 1)<...=n).toList else []

theorem Nat.toList_roc_succ_succ {m n : Nat} : ((m + 1)<...=n + 1).toList = List.map (fun (x : Nat) => x + 1) (m<...=n).toList

theorem Nat.toList_roc_succ_right_eq_cons_map {m n : Nat} (h : m ≤ n) : (m<...=n + 1).toList = (m + 1) :: List.map (fun (x : Nat) => x + 1) (m<...=n).toList

@[simp]

theorem Nat.toList_roc_eq_nil_iff {m n : Nat} : (m<...=n).toList = [] ↔ n ≤ m

theorem Nat.toList_roc_ne_nil_iff {m n : Nat} : (m<...=n).toList ≠ [] ↔ m < n

@[simp]

theorem Nat.toList_roc_eq_nil {m n : Nat} (h : n ≤ m) : (m<...=n).toList = []

@[simp]

theorem Nat.toList_roc_eq_singleton_iff {k m n : Nat} : (m<...=n).toList = [k] ↔ n = m + 1 ∧ m + 1 = k

@[simp]

theorem Nat.toList_roc_eq_singleton {m n : Nat} (h : n = m + 1) : (m<...=n).toList = [m + 1]

@[simp]

theorem Nat.toList_roc_eq_cons_iff {xs : List Nat} {m n a : Nat} : (m<...=n).toList = a :: xs ↔ m + 1 = a ∧ m < n ∧ ((m + 1)<...=n).toList = xs

theorem Nat.toList_roc_eq_cons {m n : Nat} (h : m < n) : (m<...=n).toList = (m + 1) :: ((m + 1)<...=n).toList

theorem Nat.map_add_toList_roc {m n k : Nat} : List.map (fun (x : Nat) => x + k) (m<...=n).toList = ((m + k)<...=n + k).toList

theorem Nat.map_add_toList_roc' {m n k : Nat} : List.map (fun (x : Nat) => k + x) (m<...=n).toList = ((k + m)<...=k + n).toList

theorem Nat.toList_roc_add_right_eq_map {m n : Nat} : (m<...=m + n).toList = List.map (fun (x : Nat) => x + m + 1) (0...n).toList

theorem Nat.toList_roc_succ_right_eq_append {m n : Nat} (h : m ≤ n) : (m<...=n + 1).toList = (m<...=n).toList ++ [n + 1]

theorem Nat.toList_roc_add_succ_right_eq_append {m n : Nat} : (m<...=m + n + 1).toList = (m<...=m + n).toList ++ [m + n + 1]

theorem Nat.toList_roc_add_succ_right_eq_append' {m n : Nat} : (m<...=m + (n + 1)).toList = (m<...=m + n).toList ++ [m + n + 1]

theorem Nat.toList_roc_eq_append {m n : Nat} (h : m < n) : (m<...=n).toList = (m<...=n - 1).toList ++ [n]

theorem Nat.toList_roc_add_add_eq_append {m n k : Nat} : (m<...=m + n + k).toList = (m<...=m + n).toList ++ ((m + n)<...=m + n + k).toList

theorem Nat.toList_roc_append_toList_roc {l m n : Nat} (h : l ≤ m) (h' : m ≤ n) : (l<...=m).toList ++ (m<...=n).toList = (l<...=n).toList

@[simp]

theorem Nat.getElem_toList_roc {m n i : Nat} (_h : i < (m<...=n).toList.length) : (m<...=n).toList[i] = m + 1 + i

theorem Nat.getElem?_toList_roc {m n i : Nat} : (m<...=n).toList[i]? = if i < n - m then some (m + 1 + i) else none

@[simp]

theorem Nat.getElem?_toList_roc_eq_some_iff {k m n i : Nat} : (m<...=n).toList[i]? = some k ↔ i < n - m ∧ m + 1 + i = k

@[simp]

theorem Nat.getElem?_toList_roc_eq_none_iff {m n i : Nat} : (m<...=n).toList[i]? = none ↔ n ≤ i + m

@[simp]

theorem Nat.isSome_getElem?_toList_roc_eq {m n i : Nat} : ((m<...=n).toList[i]?.isSome = true) = (i < n - m)

@[simp]

theorem Nat.isNone_getElem?_toList_roc_eq {m n i : Nat} : ((m<...=n).toList[i]?.isNone = true) = (n ≤ i + m)

@[simp]

theorem Nat.getElem?_toList_roc_eq_some {m n i : Nat} (h : i < n - m) : (m<...=n).toList[i]? = some (m + 1 + i)

@[simp]

theorem Nat.getElem?_toList_roc_eq_none {m n i : Nat} (h : n ≤ i + m) : (m<...=n).toList[i]? = none

theorem Nat.getElem!_toList_roc {m n i : Nat} : (m<...=n).toList[i]! = if i < n - m then m + 1 + i else 0

@[simp]

theorem Nat.getElem!_toList_roc_eq_add {m n i : Nat} (h : i < n - m) : (m<...=n).toList[i]! = m + 1 + i

@[simp]

theorem Nat.getElem!_toList_roc_eq_zero {m n i : Nat} (h : n ≤ i + m) : (m<...=n).toList[i]! = 0

theorem Nat.getElem!_toList_roc_eq_zero_iff {m n i : Nat} : (m<...=n).toList[i]! = 0 ↔ n ≤ i + m

theorem Nat.zero_lt_getElem!_toList_roc_iff {m n i : Nat} : 0 < (m<...=n).toList[i]! ↔ i < n - m

theorem Nat.getD_toList_roc {m n i fallback : Nat} : (m<...=n).toList.getD i fallback = if i < n - m then m + 1 + i else fallback

@[simp]

theorem Nat.getD_toList_roc_eq_add {m n i fallback : Nat} (h : i < n - m) : (m<...=n).toList.getD i fallback = m + 1 + i

@[simp]

theorem Nat.getD_toList_roc_eq_fallback {m n i fallback : Nat} (h : n ≤ i + m) : (m<...=n).toList.getD i fallback = fallback

theorem Nat.toArray_roc_eq_toArray_rcc {m n : Nat} : (m<...=n).toArray = ((m + 1)...=n).toArray

theorem Nat.toArray_roc_eq_toArray_roo {m n : Nat} : (m<...=n).toArray = (m<...n + 1).toArray

@[simp]

theorem Nat.toArray_roc_eq_toArray_rco {m n : Nat} : (m<...=n).toArray = ((m + 1)...n + 1).toArray

theorem Nat.toArray_roc_eq_if {m n : Nat} : (m<...=n).toArray = if m + 1 ≤ n then #[m + 1] ++ ((m + 1)<...=n).toArray else #[]

theorem Nat.toArray_roc_succ_succ {m n : Nat} : ((m + 1)<...=n + 1).toArray = Array.map (fun (x : Nat) => x + 1) (m<...=n).toArray

theorem Nat.toArray_roc_succ_right_eq_append_map {m n : Nat} (h : m ≤ n) : (m<...=n + 1).toArray = #[m + 1] ++ Array.map (fun (x : Nat) => x + 1) (m<...=n).toArray

@[simp]

theorem Nat.toArray_roc_eq_nil_iff {m n : Nat} : (m<...=n).toArray = #[] ↔ n ≤ m

theorem Nat.toArray_roc_ne_nil_iff {m n : Nat} : (m<...=n).toArray ≠ #[] ↔ m < n

@[simp]

theorem Nat.toArray_roc_eq_nil {m n : Nat} (h : n ≤ m) : (m<...=n).toArray = #[]

@[simp]

theorem Nat.toArray_roc_eq_singleton_iff {k m n : Nat} : (m<...=n).toArray = #[k] ↔ n = m + 1 ∧ m + 1 = k

@[simp]

theorem Nat.toArray_roc_eq_singleton {m n : Nat} (h : n = m + 1) : (m<...=n).toArray = #[m + 1]

@[simp]

theorem Nat.toArray_roc_eq_singleton_append_iff {xs : Array Nat} {m n a : Nat} : (m<...=n).toArray = #[a] ++ xs ↔ m + 1 = a ∧ m < n ∧ ((m + 1)<...=n).toArray = xs

theorem Nat.toArray_roc_eq_singleton_append {m n : Nat} (h : m < n) : (m<...=n).toArray = #[m + 1] ++ ((m + 1)<...=n).toArray

theorem Nat.map_add_toArray_roc {m n k : Nat} : Array.map (fun (x : Nat) => x + k) (m<...=n).toArray = ((m + k)<...=n + k).toArray

theorem Nat.map_add_toArray_roc' {m n k : Nat} : Array.map (fun (x : Nat) => k + x) (m<...=n).toArray = ((k + m)<...=k + n).toArray

theorem Nat.toArray_roc_add_right_eq_map {m n : Nat} : (m<...=m + n).toArray = Array.map (fun (x : Nat) => x + m + 1) (0...n).toArray

theorem Nat.toArray_roc_succ_right_eq_push {m n : Nat} (h : m ≤ n) : (m<...=n + 1).toArray = (m<...=n).toArray.push (n + 1)

theorem Nat.toArray_roc_add_succ_right_eq_push {m n : Nat} : (m<...=m + n + 1).toArray = (m<...=m + n).toArray.push (m + n + 1)

theorem Nat.toArray_roc_add_succ_right_eq_append' {m n : Nat} : (m<...=m + (n + 1)).toArray = (m<...=m + n).toArray.push (m + n + 1)

theorem Nat.toArray_roc_eq_push {m n : Nat} (h : m < n) : (m<...=n).toArray = (m<...=n - 1).toArray.push n

theorem Nat.toArray_roc_add_add_eq_append {m n k : Nat} : (m<...=m + n + k).toArray = (m<...=m + n).toArray ++ ((m + n)<...=m + n + k).toArray

theorem Nat.toArray_roc_append_toArray_roc {l m n : Nat} (h : l ≤ m) (h' : m ≤ n) : (l<...=m).toArray ++ (m<...=n).toArray = (l<...=n).toArray

@[simp]

theorem Nat.getElem_toArray_roc {m n i : Nat} (_h : i < (m<...=n).toArray.size) : (m<...=n).toArray[i] = m + 1 + i

theorem Nat.getElem?_toArray_roc {m n i : Nat} : (m<...=n).toArray[i]? = if i < n - m then some (m + 1 + i) else none

@[simp]

theorem Nat.getElem?_toArray_roc_eq_some_iff {k m n i : Nat} : (m<...=n).toArray[i]? = some k ↔ i < n - m ∧ m + 1 + i = k

@[simp]

theorem Nat.getElem?_toArray_roc_eq_none_iff {m n i : Nat} : (m<...=n).toArray[i]? = none ↔ n ≤ i + m

@[simp]

theorem Nat.isSome_getElem?_toArray_roc_eq {m n i : Nat} : ((m<...=n).toArray[i]?.isSome = true) = (i < n - m)

@[simp]

theorem Nat.isNone_getElem?_toArray_roc_eq {m n i : Nat} : ((m<...=n).toArray[i]?.isNone = true) = (n ≤ i + m)

@[simp]

theorem Nat.getElem?_toArray_roc_eq_some {m n i : Nat} (h : i < n - m) : (m<...=n).toArray[i]? = some (m + 1 + i)

@[simp]

theorem Nat.getElem?_toArray_roc_eq_none {m n i : Nat} (h : n ≤ i + m) : (m<...=n).toArray[i]? = none

theorem Nat.getElem!_toArray_roc {m n i : Nat} : (m<...=n).toArray[i]! = if i < n - m then m + 1 + i else 0

@[simp]

theorem Nat.getElem!_toArray_roc_eq_add {m n i : Nat} (h : i < n - m) : (m<...=n).toArray[i]! = m + 1 + i

@[simp]

theorem Nat.getElem!_toArray_roc_eq_zero {m n i : Nat} (h : n ≤ i + m) : (m<...=n).toArray[i]! = 0

theorem Nat.getElem!_toArray_roc_eq_zero_iff {m n i : Nat} : (m<...=n).toArray[i]! = 0 ↔ n ≤ i + m

theorem Nat.zero_lt_getElem!_toArray_roc_iff {m n i : Nat} : 0 < (m<...=n).toArray[i]! ↔ i < n - m

theorem Nat.getD_toArray_roc {m n i fallback : Nat} : (m<...=n).toArray.getD i fallback = if i < n - m then m + 1 + i else fallback

@[simp]

theorem Nat.getD_toArray_roc_eq_add {m n i fallback : Nat} (h : i < n - m) : (m<...=n).toArray.getD i fallback = m + 1 + i

@[simp]

theorem Nat.getD_toArray_roc_eq_fallback {m n i fallback : Nat} (h : n ≤ i + m) : (m<...=n).toArray.getD i fallback = fallback

theorem Nat.induct_roc_left (motive : Nat → Nat → Prop) (base : ∀ (a b : Nat), b ≤ a → motive a b) (step : ∀ (a b : Nat), a < b → motive (a + 1) b → motive a b) (a b : Nat) : motive a b

Induction principle for proving properties of Nat-based ranges of the form a<...=b by varying the lower bound.

In the base case, one proves that for any a : Nat and b : Nat with b ≤ a, the statement holds for the empty range a<...=b.

In the step case, one proves that for any a : Nat and b : Nat, the statement holds for nonempty ranges a<...=b if it holds for the smaller range (a + 1)<...=b.

The following is an example reproving length_toList_roc.

example (a b : Nat) : (a<...=b).toList.length = b - a := by
  induction a, b using Nat.induct_roc_left
  case base =>
    simp only [Nat.toList_roc_eq_nil, List.length_nil, *]; omega
  case step =>
    simp only [Nat.toList_roc_eq_cons, List.length_cons, *]; omega

theorem Nat.induct_roc_right (motive : Nat → Nat → Prop) (base : ∀ (a b : Nat), b ≤ a → motive a b) (step : ∀ (a b : Nat), a ≤ b → motive a b → motive a (b + 1)) (a b : Nat) : motive a b

Induction principle for proving properties of Nat-based ranges of the form a<...=b by varying the upper bound.

In the base case, one proves that for any a : Nat and b : Nat with b ≤ a, the statement holds for the empty range a<...=b.

In the step case, one proves that for any a : Nat and b : Nat, if the statement holds for a<...=b, it also holds for the larger range a<...=(b + 1).

The following is an example reproving length_toList_roc.

example (a b : Nat) : (a<...=b).toList.length = b - a := by
  induction a, b using Nat.induct_roc_right
  case base =>
    simp only [Nat.toList_roc_eq_nil, List.length_nil, *]; omega
  case step a b hle ih =>
    rw [Nat.toList_roc_eq_append (by omega),
      List.length_append, List.length_singleton, Nat.add_sub_cancel, ih]
    omega

@[simp]

theorem Nat.toList_rio_eq_toList_rco {n : Nat} : (*...n).toList = (0...n).toList

@[simp]

theorem Nat.toList_toArray_rio {n : Nat} : (*...n).toArray.toList = (*...n).toList

@[simp]

theorem Nat.toArray_toList_rio {n : Nat} : (*...n).toList.toArray = (*...n).toArray

theorem Nat.toList_rio_eq_if {n : Nat} : (*...n).toList = if 0 < n then (*...n - 1).toList ++ [n - 1] else []

theorem Nat.toList_rio_succ {n : Nat} : (*...n + 1).toList = (*...n).toList ++ [n]

@[simp]

theorem Nat.toList_rio_eq_nil_iff {n : Nat} : (*...n).toList = [] ↔ n = 0

theorem Nat.toList_rio_ne_nil_iff {n : Nat} : (*...n).toList ≠ [] ↔ 0 < n

@[simp]

theorem Nat.toList_rio_eq_nil {n : Nat} (h : n = 0) : (*...n).toList = []

@[simp]

theorem Nat.toList_rio_eq_singleton_iff {k n : Nat} : (*...n).toList = [k] ↔ n = 1 ∧ 0 = k

@[simp]

theorem Nat.toList_rio_one_eq_singleton : (*...1).toList = [0]

@[simp]

theorem Nat.toList_rio_eq_cons_iff {xs : List Nat} {n a : Nat} : (*...n).toList = a :: xs ↔ 0 = a ∧ 0 < n ∧ (1...n).toList = xs

theorem Nat.toList_rio_eq_cons {n : Nat} (h : 0 < n) : (*...n).toList = 0 :: (1...n).toList

@[simp]

theorem Nat.toList_rio_zero_right_eq_nil {m : Nat} : (m...0).toList = []

theorem Nat.map_add_toList_rio {n k : Nat} : List.map (fun (x : Nat) => x + k) (*...n).toList = (k...n + k).toList

theorem Nat.map_add_toList_rio' {n k : Nat} : List.map (fun (x : Nat) => k + x) (*...n).toList = (k...k + n).toList

theorem Nat.toList_rio_succ_eq_append {n : Nat} : (*...n + 1).toList = (*...n).toList ++ [n]

theorem Nat.toList_rio_eq_append {n : Nat} (h : 0 < n) : (*...n).toList = (*...n - 1).toList ++ [n - 1]

theorem Nat.toList_rio_add_add_eq_append {m n : Nat} : (*...m + n).toList = (*...m).toList ++ (m...m + n).toList

@[simp]

theorem Nat.getElem_toList_rio {n i : Nat} (_h : i < (*...n).toList.length) : (*...n).toList[i] = i

theorem Nat.getElem?_toList_rio {n i : Nat} : (*...n).toList[i]? = if i < n then some i else none

@[simp]

theorem Nat.getElem?_toList_rio_eq_some_iff {k n i : Nat} : (*...n).toList[i]? = some k ↔ i < n ∧ i = k

@[simp]

theorem Nat.getElem?_toList_rio_eq_none_iff {n i : Nat} : (*...n).toList[i]? = none ↔ n ≤ i

@[simp]

theorem Nat.isSome_getElem?_toList_rio_eq {n i : Nat} : ((*...n).toList[i]?.isSome = true) = (i < n)

@[simp]

theorem Nat.isNone_getElem?_toList_rio_eq {n i : Nat} : ((*...n).toList[i]?.isNone = true) = (n ≤ i)

@[simp]

theorem Nat.getElem?_toList_rio_eq_some {n i : Nat} (h : i < n) : (*...n).toList[i]? = some i

@[simp]

theorem Nat.getElem?_toList_rio_eq_none {n i : Nat} (h : n ≤ i) : (*...n).toList[i]? = none

theorem Nat.getElem!_toList_rio {n i : Nat} : (*...n).toList[i]! = if i < n then i else 0

@[simp]

theorem Nat.getElem!_toList_rio_eq_self {n i : Nat} (h : i < n) : (*...n).toList[i]! = i

@[simp]

theorem Nat.getElem!_toList_rio_eq_zero {n i : Nat} (h : n ≤ i) : (*...n).toList[i]! = 0

theorem Nat.getElem!_toList_rio_eq_zero_iff {n i : Nat} : (*...n).toList[i]! = 0 ↔ n ≤ i ∨ i = 0

theorem Nat.zero_lt_getElem!_toList_rio_iff {n i : Nat} : 0 < (*...n).toList[i]! ↔ i < n ∧ 0 < i

theorem Nat.getD_toList_rio {n i fallback : Nat} : (*...n).toList.getD i fallback = if i < n then i else fallback

@[simp]

theorem Nat.getD_toList_rio_eq_self {n i fallback : Nat} (h : i < n) : (*...n).toList.getD i fallback = i

@[simp]

theorem Nat.getD_toList_rio_eq_fallback {n i fallback : Nat} (h : n ≤ i) : (*...n).toList.getD i fallback = fallback

@[simp]

theorem Nat.toArray_rio_eq_toArray_rco {n : Nat} : (*...n).toArray = (0...n).toArray

theorem Nat.toArray_rio_eq_if {n : Nat} : (*...n).toArray = if 0 < n then (*...n - 1).toArray.push (n - 1) else #[]

theorem Nat.toArray_rio_succ {n : Nat} : (*...n + 1).toArray = (*...n).toArray ++ [n]

@[simp]

theorem Nat.toArray_rio_eq_nil_iff {n : Nat} : (*...n).toArray = #[] ↔ n = 0

theorem Nat.toArray_rio_ne_nil_iff {n : Nat} : (*...n).toArray ≠ #[] ↔ 0 < n

@[simp]

theorem Nat.toArray_rio_eq_nil {n : Nat} (h : n = 0) : (*...n).toArray = #[]

@[simp]

theorem Nat.toArray_rio_eq_singleton_iff {k n : Nat} : (*...n).toArray = #[k] ↔ n = 1 ∧ 0 = k

@[simp]

theorem Nat.toArray_rio_one_eq_singleton : (*...1).toArray = #[0]

@[simp]

theorem Nat.toArray_rio_eq_singleton_append_iff {xs : Array Nat} {n a : Nat} : (*...n).toArray = #[a] ++ xs ↔ 0 = a ∧ 0 < n ∧ (1...n).toArray = xs

theorem Nat.toArray_rio_eq_singleton_append {n : Nat} (h : 0 < n) : (*...n).toArray = #[0] ++ (1...n).toArray

@[simp]

theorem Nat.toArray_rio_zero_right_eq_nil {m : Nat} : (m...0).toArray = #[]

theorem Nat.map_add_toArray_rio {n k : Nat} : Array.map (fun (x : Nat) => x + k) (*...n).toArray = (k...n + k).toArray

theorem Nat.map_add_toArray_rio' {n k : Nat} : Array.map (fun (x : Nat) => k + x) (*...n).toArray = (k...k + n).toArray

theorem Nat.toArray_rio_succ_eq_push {n : Nat} : (*...n + 1).toArray = (*...n).toArray.push n

theorem Nat.toArray_rio_eq_push {n : Nat} (h : 0 < n) : (*...n).toArray = (*...n - 1).toArray.push (n - 1)

theorem Nat.toArray_rio_add_add_eq_append {m n : Nat} : (*...m + n).toArray = (*...m).toArray ++ (m...m + n).toArray

@[simp]

theorem Nat.getElem_toArray_rio {n i : Nat} (_h : i < (*...n).toArray.size) : (*...n).toArray[i] = i

theorem Nat.getElem?_toArray_rio {n i : Nat} : (*...n).toArray[i]? = if i < n then some i else none

@[simp]

theorem Nat.getElem?_toArray_rio_eq_some_iff {k n i : Nat} : (*...n).toArray[i]? = some k ↔ i < n ∧ i = k

@[simp]

theorem Nat.getElem?_toArray_rio_eq_none_iff {n i : Nat} : (*...n).toArray[i]? = none ↔ n ≤ i

@[simp]

theorem Nat.isSome_getElem?_toArray_rio_eq {n i : Nat} : ((*...n).toArray[i]?.isSome = true) = (i < n)

@[simp]

theorem Nat.isNone_getElem?_toArray_rio_eq {n i : Nat} : ((*...n).toArray[i]?.isNone = true) = (n ≤ i)

@[simp]

theorem Nat.getElem?_toArray_rio_eq_some {n i : Nat} (h : i < n) : (*...n).toArray[i]? = some i

@[simp]

theorem Nat.getElem?_toArray_rio_eq_none {n i : Nat} (h : n ≤ i) : (*...n).toArray[i]? = none

theorem Nat.getElem!_toArray_rio {n i : Nat} : (*...n).toArray[i]! = if i < n then i else 0

@[simp]

theorem Nat.getElem!_toArray_rio_eq_self {n i : Nat} (h : i < n) : (*...n).toArray[i]! = i

@[simp]

theorem Nat.getElem!_toArray_rio_eq_zero {n i : Nat} (h : n ≤ i) : (*...n).toArray[i]! = 0

theorem Nat.getElem!_toArray_rio_eq_zero_iff {n i : Nat} : (*...n).toArray[i]! = 0 ↔ n ≤ i ∨ i = 0

theorem Nat.zero_lt_getElem!_toArray_rio_iff {n i : Nat} : 0 < (*...n).toArray[i]! ↔ i < n ∧ 0 < i

theorem Nat.getD_toArray_rio {n i fallback : Nat} : (*...n).toArray.getD i fallback = if i < n then i else fallback

@[simp]

theorem Nat.getD_toArray_rio_eq_self {n i fallback : Nat} (h : i < n) : (*...n).toArray.getD i fallback = i

@[simp]

theorem Nat.getD_toArray_rio_eq_fallback {n i fallback : Nat} (h : n ≤ i) : (*...n).toArray.getD i fallback = fallback

theorem Nat.toList_ric_eq_toList_rio {n : Nat} : (*...=n).toList = (*...n + 1).toList

theorem Nat.toList_ric_eq_toList_rcc {n : Nat} : (*...=n).toList = (*...n + 1).toList

@[simp]

theorem Nat.toList_ric_eq_toList_rco {n : Nat} : (*...=n).toList = (0...n + 1).toList

@[simp]

theorem Nat.toList_toArray_ric {n : Nat} : (*...=n).toArray.toList = (*...=n).toList

@[simp]

theorem Nat.toArray_toList_ric {n : Nat} : (*...=n).toList.toArray = (*...=n).toArray

theorem Nat.toList_ric_eq_toList_rio_append {n : Nat} : (*...=n).toList = (*...n).toList ++ [n]

theorem Nat.toList_ric_succ {n : Nat} : (*...=n + 1).toList = (*...=n).toList ++ [n + 1]

@[simp]

theorem Nat.toList_ric_ne_nil {n : Nat} : (*...=n).toList ≠ []

@[simp]

theorem Nat.toList_ric_eq_singleton_iff {k n : Nat} : (*...=n).toList = [k] ↔ n = 0 ∧ 0 = k

@[simp]

theorem Nat.toList_ric_zero_eq_singleton : (*...=0).toList = [0]

@[simp]

theorem Nat.toList_ric_eq_cons_iff {xs : List Nat} {n a : Nat} : (*...=n).toList = a :: xs ↔ 0 = a ∧ (1...=n).toList = xs

theorem Nat.toList_ric_eq_cons {n : Nat} : (*...=n).toList = 0 :: (1...=n).toList

theorem Nat.map_add_toList_ric {n k : Nat} : List.map (fun (x : Nat) => x + k) (*...=n).toList = (k...=n + k).toList

theorem Nat.map_add_toList_ric' {n k : Nat} : List.map (fun (x : Nat) => k + x) (*...=n).toList = (k...=k + n).toList

theorem Nat.toList_ric_succ_eq_append {n : Nat} : (*...=n + 1).toList = (*...=n).toList ++ [n + 1]

theorem Nat.toList_ric_eq_append {n : Nat} (h : 0 < n) : (*...=n).toList = (*...=n - 1).toList ++ [n]

theorem Nat.toList_ric_add_add_eq_append {m n : Nat} : (*...=m + n).toList = (*...m).toList ++ (m...=m + n).toList

@[simp]

theorem Nat.getElem_toList_ric {n i : Nat} (_h : i < (*...=n).toList.length) : (*...=n).toList[i] = i

theorem Nat.getElem?_toList_ric {n i : Nat} : (*...=n).toList[i]? = if i ≤ n then some i else none

@[simp]

theorem Nat.getElem?_toList_ric_eq_some_iff {k n i : Nat} : (*...=n).toList[i]? = some k ↔ i ≤ n ∧ i = k

@[simp]

theorem Nat.getElem?_toList_ric_eq_none_iff {n i : Nat} : (*...=n).toList[i]? = none ↔ n < i

@[simp]

theorem Nat.isSome_getElem?_toList_ric_eq {n i : Nat} : ((*...=n).toList[i]?.isSome = true) = (i ≤ n)

@[simp]

theorem Nat.isNone_getElem?_toList_ric_eq {n i : Nat} : ((*...=n).toList[i]?.isNone = true) = (n < i)

@[simp]

theorem Nat.getElem?_toList_ric_eq_some {n i : Nat} (h : i ≤ n) : (*...=n).toList[i]? = some i

@[simp]

theorem Nat.getElem?_toList_ric_eq_none {n i : Nat} (h : n < i) : (*...=n).toList[i]? = none

theorem Nat.getElem!_toList_ric {n i : Nat} : (*...=n).toList[i]! = if i ≤ n then i else 0

@[simp]

theorem Nat.getElem!_toList_ric_eq_self {n i : Nat} (h : i ≤ n) : (*...=n).toList[i]! = i

@[simp]

theorem Nat.getElem!_toList_ric_eq_zero {n i : Nat} (h : n < i) : (*...=n).toList[i]! = 0

theorem Nat.getElem!_toList_ric_eq_zero_iff {n i : Nat} : (*...=n).toList[i]! = 0 ↔ n < i ∨ i = 0

theorem Nat.zero_lt_getElem!_toList_ric_iff {n i : Nat} : 0 < (*...=n).toList[i]! ↔ i ≤ n ∧ 0 < i

theorem Nat.getD_toList_ric {n i fallback : Nat} : (*...=n).toList.getD i fallback = if i ≤ n then i else fallback

@[simp]

theorem Nat.getD_toList_ric_eq_self {n i fallback : Nat} (h : i ≤ n) : (*...=n).toList.getD i fallback = i

@[simp]

theorem Nat.getD_toList_ric_eq_fallback {n i fallback : Nat} (h : n < i) : (*...=n).toList.getD i fallback = fallback

theorem Nat.toArray_ric_eq_toArray_rio {n : Nat} : (*...=n).toArray = (*...n + 1).toArray

theorem Nat.toArray_ric_eq_toArray_rcc {n : Nat} : (*...=n).toArray = (*...n + 1).toArray

@[simp]

theorem Nat.toArray_ric_eq_toArray_rco {n : Nat} : (*...=n).toArray = (0...n + 1).toArray

theorem Nat.toArray_ric_eq_toArray_rio_push {n : Nat} : (*...=n).toArray = (*...n).toArray.push n

theorem Nat.toArray_ric_succ {n : Nat} : (*...=n + 1).toArray = (*...=n).toArray.push (n + 1)

@[simp]

theorem Nat.toArray_ric_ne_nil {n : Nat} : (*...=n).toArray ≠ #[]

@[simp]

theorem Nat.toArray_ric_eq_singleton_iff {k n : Nat} : (*...=n).toArray = #[k] ↔ n = 0 ∧ 0 = k

@[simp]

theorem Nat.toArray_ric_zero_eq_singleton : (*...=0).toArray = #[0]

@[simp]

theorem Nat.toArray_ric_eq_singleton_append_iff {xs : Array Nat} {n a : Nat} : (*...=n).toArray = #[a] ++ xs ↔ 0 = a ∧ (1...=n).toArray = xs

theorem Nat.toArray_ric_eq_cons {n : Nat} : (*...=n).toArray = #[0] ++ (1...=n).toArray

theorem Nat.map_add_toArray_ric {n k : Nat} : Array.map (fun (x : Nat) => x + k) (*...=n).toArray = (k...=n + k).toArray

theorem Nat.map_add_toArray_ric' {n k : Nat} : Array.map (fun (x : Nat) => k + x) (*...=n).toArray = (k...=k + n).toArray

theorem Nat.toArray_ric_succ_eq_push {n : Nat} : (*...=n + 1).toArray = (*...=n).toArray.push (n + 1)

theorem Nat.toArray_ric_eq_push {n : Nat} (h : 0 < n) : (*...=n).toArray = (*...=n - 1).toArray.push n

theorem Nat.toArray_ric_add_add_eq_append {m n : Nat} : (*...=m + n).toArray = (*...m).toArray ++ (m...=m + n).toArray

@[simp]

theorem Nat.getElem_toArray_ric {n i : Nat} (_h : i < (*...=n).toArray.size) : (*...=n).toArray[i] = i

theorem Nat.getElem?_toArray_ric {n i : Nat} : (*...=n).toArray[i]? = if i ≤ n then some i else none

@[simp]

theorem Nat.getElem?_toArray_ric_eq_some_iff {k n i : Nat} : (*...=n).toArray[i]? = some k ↔ i ≤ n ∧ i = k

@[simp]

theorem Nat.getElem?_toArray_ric_eq_none_iff {n i : Nat} : (*...=n).toArray[i]? = none ↔ n < i

@[simp]

theorem Nat.isSome_getElem?_toArray_ric_eq {n i : Nat} : ((*...=n).toArray[i]?.isSome = true) = (i ≤ n)

@[simp]

theorem Nat.isNone_getElem?_toArray_ric_eq {n i : Nat} : ((*...=n).toArray[i]?.isNone = true) = (n < i)

@[simp]

theorem Nat.getElem?_toArray_ric_eq_some {n i : Nat} (h : i ≤ n) : (*...=n).toArray[i]? = some i

@[simp]

theorem Nat.getElem?_toArray_ric_eq_none {n i : Nat} (h : n < i) : (*...=n).toArray[i]? = none

theorem Nat.getElem!_toArray_ric {n i : Nat} : (*...=n).toArray[i]! = if i ≤ n then i else 0

@[simp]

theorem Nat.getElem!_toArray_ric_eq_self {n i : Nat} (h : i ≤ n) : (*...=n).toArray[i]! = i

@[simp]

theorem Nat.getElem!_toArray_ric_eq_zero {n i : Nat} (h : n < i) : (*...=n).toArray[i]! = 0

theorem Nat.getElem!_toArray_ric_eq_zero_iff {n i : Nat} : (*...=n).toArray[i]! = 0 ↔ n < i ∨ i = 0

theorem Nat.zero_lt_getElem!_toArray_ric_iff {n i : Nat} : 0 < (*...=n).toArray[i]! ↔ i ≤ n ∧ 0 < i

theorem Nat.getD_toArray_ric {n i fallback : Nat} : (*...=n).toArray.getD i fallback = if i ≤ n then i else fallback

@[simp]

theorem Nat.getD_toArray_ric_eq_self {n i fallback : Nat} (h : i ≤ n) : (*...=n).toArray.getD i fallback = i

@[simp]

theorem Nat.getD_toArray_ric_eq_fallback {n i fallback : Nat} (h : n < i) : (*...=n).toArray.getD i fallback = fallback

theorem List.range_eq_toList_rco {n : Nat} : range n = (0...n).toList

theorem List.range'_eq_toList_rco {m n : Nat} : range' m n = (m...m + n).toList

theorem Array.range_eq_toArray_rco {n : Nat} : range n = (0...n).toArray

theorem Array.range'_eq_toArray_rco {m n : Nat} : range' m n = (m...m + n).toArray