theorem Array.sizeOf_head?_of_mem {α : Type u_1} {a : α} {as' : Array α} [SizeOf α] {as : Array α} (h : as.head? = some (a, as')) : sizeOf a < sizeOf as

theorem Array.sizeOf_head?_of_tail {α : Type u_1} {a : α} {as' : Array α} [SizeOf α] {as : Array α} (h : as.head? = some (a, as')) : sizeOf as' < sizeOf as

theorem Array.sizeOf_dropLast_cons {α : Type u_1} [SizeOf α] (a : α) (as : List α) : sizeOf (a :: as).dropLast < sizeOf (a :: as)

theorem Array.sizeOf_dropLast_non_empty {α : Type u_1} [SizeOf α] (as : List α) (h : 0 < as.length) : sizeOf as.dropLast < sizeOf as

theorem Array.sizeOf_pop_non_empty {α : Type u_1} [SizeOf α] (as : Array α) (h : 0 < as.data.length) : sizeOf as.pop < sizeOf as

theorem Array.sizeOf_pop? {α : Type u_1} {a : α} {as' : Array α} [SizeOf α] {as : Array α} (h : as.pop? = some (a, as')) : sizeOf as' < sizeOf as

theorem Array.size_one {α : Type u_1} (a : α) : #[a].size = 1

theorem Array.default_size_zero {α : Type u_1} (arr : Array α) (h : arr = default) : arr.size = 0

theorem Array.non_empty_of_last? {α : Type u_1} {last : α} (arr : Array α) (h : arr.last? = some last) : 0 < arr.size

theorem Array.pop?_of_last? {α : Type u_1} {last : α} (arr : Array α) (h : arr.last? = some last) : ∃ (arr' : Array α), arr.pop? = some (last, arr')

theorem Array.pop?_of_non_empty {α : Type u_1} (arr : Array α) (h : 0 < arr.size) : ∃ (arr' : Array α), ∃ (last : α), arr.pop? = some (last, arr')

theorem Array.last?_eq_getLast {α : Type u_1} {last : α} (a : Array α) (h1 : a.last? = some last) (h2 : a.data ≠ []) : a.data.getLast h2 = last

theorem Array.lt_of_pop?_eq_last? {α : Type u_1} {last : α} {arr' : Array α} {arr : Array α} (h : arr.pop? = some (last, arr')) : 0 < arr.data.length

theorem Array.get_last_of_pop? {α : Type u_1} {last : α} {arr' : Array α} {arr : Array α} (h1 : arr.pop? = some (last, arr')) (h2 : arr.data.length - 1 < arr.data.length) : arr.data.get ⟨arr.data.length - 1, h2⟩ = last

theorem Array.concat_of_pop? {α : Type u_1} {last : α} {arr' : Array α} {arr : Array α} (h : arr.pop? = some (last, arr')) : arr.data = arr'.data ++ [last]