## Half-minus -

The half minus operation is similar to normal subtraction, but it operates on natural numbers so it does not return negative numbers. When (>= a b), (.- a b) is just like normal subtraction, but when (< a b) then (= (.- a b) (0)) /edit/peano/peano_thms.gh/halfminus-neg.

### Important Theorems

• Cancellation: (= (.- a a) (0)) /edit/peano_new/arithmetic/naturals/halfminus.gh/halfminusid
• Cancellation: (= (.- (+ a b) b) a) /edit/peano_new/arithmetic/naturals/halfminus.gh/halfminuscan
• Cancellation: (-> (<= b a) (= (+ (.- a b) b) a)) /edit/peano_new/arithmetic/naturals/halfminus.gh/halfminus
• Half-Minus Never Goes Negative: (-> (<= a b) (= (.- a b) (0))) /edit/peano/peano_thms.gh/halfminus-neg

### Example

• (= (.- (+ (* (2) (* (10) (10))) (+ (* (4) (10)) (3))) (+ (* (10) (10)) (+ (* (8) (10)) (6)))) (+ (* (5) (10)) (7))) /edit/peano/arithmetic.gh/halfMinusExample
• (= (.- (+ (* (10) (10)) (+ (* (8) (10)) (6))) (+ (* (2) (* (10) (10))) (+ (* (4) (10)) (3)))) (0)) /edit/peano/arithmetic.gh/halfMinusExample2