subtype in order/lattices

[hivert]

I'm afraid I might be not expert enough with canonical structure to finish my pull request #8. Here is what could possibly done

1 - Any subtype of a porder/order and their finite version is canonically ordered. Except correctly dealing with canonicals there is nearly nothing to do here. Example of application : 'I_n, tuple...
2 - define a notion of lattice_closed saying that sup and inf are compatible with a predicate
3 - this allows to define a notion of sublattice

For me 1 is a prerequisite to switch to finmap what I did in https://github.com/hivert/Coq-Combi.