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.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.