for a, b being natural Number holds a -' b <= a