1. Define natural numbers inductively with type mynat. 2. Define the notion and semantics of a predicate greater-than-or-equal-to (>=) over mynat with type mynat -> mynat -> Prop. 3. Use above definitions to prove that if n >= m => n+1 >= m+1. Submission: coq script Get Coq: http://coq.inria.fr/ References: http://coq.inria.fr/V8.1/tutorial.html [Intranet] http://poorvi.cse.iitd.ac.in/~dahiya/ (more useful references may be put here later) Due date: Oct. 28, 2013