Introduce function to compute nth element of a chain

This should make mid drop etc much easier
Prove decidability of even or odd
Move Even and Odd code to Misc.agda
Merge branch 'master' into nth-function
Introduce div2 - division by two for even numbers
Prove div2 n \leq n
Begin rewrite

Introduce a parameter to the chain type - length of the chain

Reverse the chain cons constructor - chain now grows to the left
Introduce init and tail functions without depending on reverse
Make parameter to nth function implicit
Make cons operator right associative
Huge rewrite

- chain construction now uses incidence proof as the term. The elements
can be inferred form it anyway.
- Include length of the chain in the datatype definition
- Made \in and irred into their own inductive datatypes
- Use inductive type to enforce incidence condition on Incidence
Planes. This forces us to make the incidence proof object in the chain
constructor relevant.
Define equality of chains.

Ignore the proof of incidence. Only points matter.
Introduce axioms for Generalised Polygon
Merge branch 'nth-function'