Enter a Coq theorem to prove, or select an example from the drop-down menu
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 is working...