Basic lemmas about built-in types

ink

theorem List.fold_max_max_eq_max_fold_max {xs : List ℕ} {a : ℕ} {b : ℕ} : List.foldl max (max a b) xs = max a (List.foldl max b xs)

ink

theorem List.get_index_eq {α : Type u_1} {xs : List α} {i : ℕ} {j : ℕ} (hi : i < List.length xs) (h : i = j) : ∃ hj, List.get xs { val := i, isLt := hi } = List.get xs { val := j, isLt := hj }

ink

theorem List.get_zero_eq_head {α : Type u_1} {xs : List α} (hn : xs ≠ []) : List.get xs { val := 0, isLt := (_ : 0 < List.length xs) } = List.head xs hn

ink

theorem Nat.not_lt_of_lt {a : ℕ} {b : ℕ} (h : a < b) : ¬b < a

ink

theorem Nat.mul_lt_mul₀ {a : ℕ} {b : ℕ} {c : ℕ} {d : ℕ} (h1 : a < c) (h2 : b < d) : a * b < c * d

ink

theorem Nat.sub_lt_sub_right {a : ℕ} {b : ℕ} {c : ℕ} (h0 : a < b) (h1 : c ≤ a) : a - c < b - c

ink

theorem Nat.sub_sub_eq {a : ℕ} {b : ℕ} {c : ℕ} (h : a ≤ b) : c + a - b = c - (b - a)