Min and max relations in the numerical sort

I attach an executable compiled under AMD64 (aka. x86_64) and Linux 3.11. The manual can also be found in the doc directory.

Changes:

• Several bug fixes.
• So-called "opti" relations: k=min(m,n) and k=max(m,n) in the num sort, with general form in concrete syntax min|max(m-k,n-k), resp. min|max(k-m,k-n).
• So-called "subopti" relations k<=max(m,n) and min(m,n)<=k in the num sort, with general form in concrete syntax min||max(m-k,n-k), resp. min||max(k-m,k-n).
• Less confusing syntax: datatype and datacons keywords, existential types.
• Pattern-matching guards when e1 <= e2, where e1 and e2 are expressions of type Num.
• Positive assert clauses, assert num e1 <= e2; ... and assert type e1 = e2; ....
• Flagship example: AVL trees with imbalance of 2 (based on the implementation from OCaml standard library).