Enter your own theorem Every element of a list of natural numbers is non-negative 0 = 5 is false Appending an empty list to a list results in that list every_elem_le_max: Every element of a list is less than or equal to the list's max list_forall2_app: If property P holds on corresponding pairs from lists a1, b1 and a2, b2, P also holds on pairs from a1a2, b1b2 list_forall2_app with induction hint

Following the theorem statement, start the proof with “Proof.” and “Admitted.”
Proofster will attempt to replace “Admitted.” with a Coq proof.

Proofster it!