Adds FinToNatLt

This function gives a proof that for n : Fin k, finToNat n < k.