Create a project in Coq interactive theorem prover

For the project option. The requirements are: 1. Identify some non-trivial theorem or sets of theorems that aren't from SF or proven in Coq by someone else. 2. Formalize it in Coq along with any associated definitions. 3. Prove your theorem to Coq's satisfaction. 4. Write a short report (a page or two is fine) describing the significance of your theorem/definitions and any interesting technical issues you ran into in formalize your definitions, theorems, or proofs in Coq. 5. A short presentation (~ 5-10 minutes) during the course's final exam period. - If the project consists of one theorem that can be proven with "eauto; solve by inversion". Then its probably too trivial, i.e. not "non-trivial". - A project might be "interesting" because of the non-PL 'application' of the theorem, the inductive data types that it works with, and/or the proof techniques. My intent isn't to set an extremely high bar here. A quick turn around would be nice along with the document to present for the project. Please don't look at the skill set needed as I was not able to mention what was needed for Coq in there.