An example of rank computation.

Created pivot.v, meant to describe various pivot search strategies and prove
their correctness.

More work to be done on automation, which doesn't quite work properly,
and on cleaning the code.
Add pivot and funperm in build process.