Changed definition of LessNat from n + suc k to suc k + n

This makes it easier to prove not (n < zero) and
LessThan n < suc n, but harder to prove n < m <=> suc n < suc m.
Functor and Traversable for Data.Reflect.Arg
Added Control.WellFounded

Accessibility definition and well-foundedness proof for NatLess.