49. A nonempty list has a first element

EasyProofFree10 points

xs.head? is none for the empty list and some x for a list that starts with x. Prove that it is not none when xs is not empty.

Solution.lean

1theorem solution (xs : List Nat) (h : xs ≠ []) : xs.head? ≠ none := by

given

Loading editor…

Where you start. Everything above ⊢ may be assumed; the line below it is what you must prove.

xs:List Nat

h:xs ≠ []

⊢xs.head? ≠ none

ReadyLn 1, Col 1Lean 4

Draft saved in this browser