split off Basics/Decidable.v, with a few new lemmas in it

I thought it would be nice to keep it, to remind the reader that our `not` is different from the one in the stdlib.