Duality Tactic for Lattice Theory

This new Coq tactic duality allows you to prove a lattice theory (in)equality if its dual has already been proven.

For a demo:

1. Compile with make clean; make.
2. Run Duality.v either from the command line, or from the Coq IDE.

Tested on Coq version 8.9.0.