@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

@[simp]

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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

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

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

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

@[simp]

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

@[simp]

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

@[simp]

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

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

theorem Int.getElem!_toList_rco_ne_zero_iff {m n : Int} {i : Nat} : (m...n).toList[i]! ≠ 0 ↔ i < (n - m).toNat ∧ m + ↑i ≠ 0

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

@[simp]

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

@[simp]

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

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

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

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

@[simp]

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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

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

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

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

@[simp]

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

@[simp]

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

@[simp]

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

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

theorem Int.getElem!_toArray_rco_ne_zero_iff {m n : Int} {i : Nat} : (m...n).toArray[i]! ≠ 0 ↔ i < (n - m).toNat ∧ m + ↑i ≠ 0

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

@[simp]

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

@[simp]

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

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

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

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

In the step case, one proves that for any a : Int and b : Int, 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 : Int) : (a...b).toList.length = (b - a).toNat := by
  induction a, b using Int.induct_rco_left
  case base =>
    simp [Int.toList_rco_eq_nil, List.length_nil, Int.zero_eq_toNat_sub_iff, *]
  case step =>
    simp only [Int.toList_rco_eq_cons, List.length_cons, *]; omega

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

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

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

In the step case, one proves that for any a : Int and b : Int, 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 : Int) : (a...b).toList.length = (b - a).toNat := by
  induction a, b using Int.induct_rco_right
  case base =>
    simp only [Int.toList_rco_eq_nil, List.length_nil, Int.zero_eq_toNat_sub_iff, *]
  case step a b hle ih =>
    rw [Int.toList_rco_eq_append (by omega),
      List.length_append, List.length_singleton, Int.add_sub_cancel, ih]
    omega

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

@[simp]

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

@[simp]

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

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

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

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

@[simp]

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

@[simp]

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

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

@[simp]

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

@[simp]

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

@[simp]

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

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

theorem Int.getElem!_toList_rcc_ne_zero_iff {m n : Int} {i : Nat} : (m...=n).toList[i]! ≠ 0 ↔ i < (n + 1 - m).toNat ∧ m + ↑i ≠ 0

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

@[simp]

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

@[simp]

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

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

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

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

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

@[simp]

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

@[simp]

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

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

@[simp]

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

@[simp]

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

@[simp]

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

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

theorem Int.getElem!_toArray_rcc_ne_zero_iff {m n : Int} {i : Nat} : (m...=n).toArray[i]! ≠ 0 ↔ i < (n + 1 - m).toNat ∧ m + ↑i ≠ 0

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

@[simp]

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

@[simp]

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

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

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

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

In the step case, one proves that for any a : Int and b : Int, 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 : Int) : (a...=b).toList.length = (b + 1 - a).toNat := by
  induction a, b using Int.induct_rcc_left
  case base =>
    simp only [Int.toList_rcc_eq_nil, List.length_nil, Int.zero_eq_toNat_sub_iff, *]; omega
  case step =>
    simp only [Int.toList_rcc_eq_cons, List.length_cons, *]; omega

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

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

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

In the step case, one proves that for any a : Int and b : Int, 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 : Int) : (a...=b).toList.length = (b + 1 - a).toNat := by
  induction a, b using Int.induct_rcc_right
  case base a b hge =>
    by_cases h : b < a
    · simp only [Int.toList_rcc_eq_nil, List.length_nil, *]
      omega
    · have : b = a := by omega
      simp only [Int.toList_rcc_eq_singleton, List.length_singleton,
        Int.sub_eq_iff_eq_add'.mpr rfl, Int.toNat_one, *]
  case step a b hle ih =>
    rw [Int.toList_rcc_succ_right_eq_append (by omega), List.length_append,
      List.length_singleton, ih] <;> omega

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

@[simp]

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

@[simp]

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

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

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

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

@[simp]

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

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

@[simp]

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

@[simp]

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

@[simp]

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

@[simp]

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

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

theorem Int.zero_ne_getElem!_toList_roo_iff {m n : Int} {i : Nat} : (m<...n).toList[i]! ≠ 0 ↔ i < (n - (m + 1)).toNat ∧ m + ↑i ≠ -1

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

@[simp]

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

@[simp]

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

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

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

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

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

@[simp]

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

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

@[simp]

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

@[simp]

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

@[simp]

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

@[simp]

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

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

theorem Int.getElem!_toArray_roo_ne_zero_iff {m n : Int} {i : Nat} : (m<...n).toArray[i]! ≠ 0 ↔ i < (n - (m + 1)).toNat ∧ m + ↑i ≠ -1

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

@[simp]

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

@[simp]

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

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

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

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

In the step case, one proves that for any a : Int and b : Int, 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 : Int) : (a<...b).toList.length = (b - a - 1).toNat := by
  induction a, b using Int.induct_roo_left
  case base =>
    simp only [Int.toList_roo_eq_nil, List.length_nil, Int.zero_eq_toNat_sub_iff, *]; omega
  case step =>
    simp only [Int.toList_roo_eq_cons, List.length_cons, *]; omega

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

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

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

In the step case, one proves that for any a : Int and b : Int, 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 : Int) : (a<...b).toList.length = (b - a - 1).toNat := by
  induction a, b using Int.induct_roo_right
  case base =>
    simp only [Int.toList_roo_eq_nil, List.length_nil, *]; omega
  case step a b hle ih =>
    rw [Int.toList_roo_eq_append (by omega),
      List.length_append, List.length_singleton, Int.add_sub_cancel, ih]
    omega

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

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

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

@[simp]

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

@[simp]

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

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

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

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

@[simp]

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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

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

@[simp]

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

@[simp]

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

@[simp]

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

theorem Int.getElem!_toList_roc_eq_zero_iff {m n : Int} {i : Nat} : (m<...=n).toList[i]! = 0 ↔ (n - m).toNat ≤ i ∨ m + ↑i = -1

theorem Int.getElem!_toList_roc_ne_zero_iff {m n : Int} {i : Nat} : (m<...=n).toList[i]! ≠ 0 ↔ i < (n - m).toNat ∧ m + ↑i ≠ -1

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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

@[simp]

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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

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

@[simp]

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

@[simp]

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

@[simp]

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

theorem Int.getElem!_toArray_roc_eq_zero_iff {m n : Int} {i : Nat} : (m<...=n).toArray[i]! = 0 ↔ (n - m).toNat ≤ i ∨ m + ↑i = -1

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

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

@[simp]

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

@[simp]

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

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

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

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

In the step case, one proves that for any a : Int and b : Int, 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 : Int) : (a<...=b).toList.length = (b - a).toNat := by
  induction a, b using Int.induct_roc_left
  case base =>
    simp only [Int.toList_roc_eq_nil, List.length_nil, Int.zero_eq_toNat_sub_iff, *]
  case step =>
    simp only [Int.toList_roc_eq_cons, List.length_cons, *]; omega

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

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

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

In the step case, one proves that for any a : Int and b : Int, 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 : Int) : (a<...=b).toList.length = (b - a).toNat := by
  induction a, b using Int.induct_roc_right
  case base =>
    simp only [Int.toList_roc_eq_nil, List.length_nil, Int.zero_eq_toNat_sub_iff, *]
  case step a b hle ih =>
    rw [Int.toList_roc_eq_append (by omega),
      List.length_append, List.length_singleton, Int.add_sub_cancel, ih]
    omega