Introduce notation for shortest chain
Major rewrite

Major rewrite which includes

- Changed notation for chain constructor
- Make irred \in etc as functions as opposed to data types
- Notion of shortest chain and proof of its irreducibility
- Theorems on length of shortest chain in case of Incidence Plane
Merge branch 'irred'