Add definition and basic thms for halfminus
Add definition and basic thms for halfminus

A definition of "halfminus" which works over the natural numbers.

raphlinus/ghilbert,raphlinus/ghilbert,raphlinus/ghilbert,raphlinus/ghilbert