stuck with a proof

You need to do the math correctly first: find two functions that are inverse of each other.

You initial intent is correct: odd numbers to one side, even numbers to the other side, but what you store on each side should cover all the natural numbers, so you will probably have to divide by 2 somewhere.

For Coq usage, You should load the `Arith` package, by starting with the following line:

``````Require Import Arith.
``````

This way, you can benefit from existing functions, like `Nat.div2` and `Nat.even` and all the existing theorems about them. To find the relevant theorems, I suggest commands like:

``````Search Nat.even 2.
Search Nat.div2.
``````

Last hint: proving properties of `Nat.div2` by induction is rather difficult for beginners. Try to use the existing theorems as much as possible. If you choose to perform a proof by induction concerning `div2`, go look in the sources in file `theories/Arith/Div2.v` : the author of that file designed a specific induction theorem called `ìnd_0_1_SS` just for that purpose.

CLICK HERE to find out more related problems solutions.

Scroll to Top