Results about List.sum specialized to Nat

theorem List.find?_eq_some_iff_getElem {α : Type u_1} {xs : List α} {p : α → Bool} {b : α} : find? p xs = some b ↔ p b = true ∧ ∃ (i : Nat), ∃ (h : i < xs.length), xs[i] = b ∧ ∀ (j : Nat) (hj : j < i), (!p xs[j]) = true

theorem List.findIdx?_eq_some_le_of_findIdx?_eq_some {α : Type u_1} {xs : List α} {p q : α → Bool} (w : ∀ (x : α), x ∈ xs → p x = true → q x = true) {i : Nat} (h : findIdx? p xs = some i) : ∃ (j : Nat), j ≤ i ∧ findIdx? q xs = some j