FinFun.v: results about injective/surjective/bijective fonctions over finite domains

 + Some extra results about NoDup, Fin.t, ...