Proofs of specification for functions defined over Vector
Author: Pierre Boutillier
Institution: PPS, INRIA 12/2010
Lemmas are done for functions that use
Fin.t but thanks to
Peano_dec.le_unique, all
is true for the one that use
lt
Properties of nth and nth_order