# List of theorems

List of theorems in peano_new/arithmetic/naturals/halfminus.gh:

## Subtraction over natural numbers

df-halfminus-just Justification for definition of halfminus
(= (ifn (< A B) (0) (iota ({|} x (= A (+ B x))))) (ifn (< A B) (0) (iota ({|} y (= A (+ B y))))))
df-halfminus Definition of "half minus"
(= (.- A B) (ifn (< A B) (0) (iota ({|} x (= A (+ B x))))))
EqReplaceImp1Eq0 # <title> Substitution </title> # <table> # (-> ph (= [ A ] ] ] C)) # (= [ A ] [ B ] ) # (-> ph (= [ [ [ B ] C)) # </table>
(-> ph (= A C)) , (= A B)(-> ph (= B C))
EqReplaceImp1Eq1 # <title> Substitution </title> # <table> # (-> ph (= A [ B ] ] ] )) # (= [ B ] [ C ] ) # (-> ph (= A [ [ [ C ] )) # </table>
(-> ph (= A B)) , (= B C)(-> ph (= A C))
(-> (= A C) (= (.- A B) (.- C B)))
(= A B)(= (.- A C) (.- B C))
(-> ph (= A B))(-> ph (= (.- A C) (.- B C)))
halfminuseq2 # <title> Equivalence for - </title>
(-> (= B C) (= (.- A B) (.- A C)))
(= B C)(= (.- A B) (.- A C))
(-> ph (= B C))(-> ph (= (.- A B) (.- A C)))
(-> (/\ (= A B) (= C D)) (= (.- A C) (.- B D)))
ImpReplaceBi1 # <title> Substitution </title> # <table> # (<-> ph [ ps ] ] ] ) # (-> [ ps ] [ ch ] ) # (<-> ph [ [ [ ch ] ) # </table>
(<-> ph ps) , (-> ps ch)(-> ph ch)
ImpReplaceBi1Ex1 # <title> Substitution </title> # <table> # (<-> ph (E. x [ ps ] ] ] )) # (-> [ ps ] [ ch ] ) # (<-> ph (E. x [ [ [ ch ] )) # </table>
(<-> ph (E. x ps)) , (-> ps ch)(-> ph (E. x ch))
eudiff # <title> The difference between two numbers is unique </title>
(-> (<= B A) (E! x (= A (+ B x))))
halfminus # <title> Minus is the inverse of addition </title>
(-> (<= B A) (= (+ (.- A B) B) A))
halfminusid # <title> A number minus itself is zero </title> # <suggest> right('Cancel', '-') </suggest> # <table> # (= (.- <r> A <r> A) (0)) # </table>
(= (.- A A) (0))
EqReplaceLe0 # <title> Substitution </title> # <table> # (<= [ A ] ] ] C) # (= [ A ] [ B ] ) # (<= [ [ [ B ] C) # </table>
(<= A C) , (= A B)(<= B C)
halfminuszero # <title> A number minus zero is itself </title>
(= (.- A (0)) A)
halfminuscan # <title> Half minus cancellation </title> # <suggest> right('Simplify', '-') </suggest> # <table> # (= (.- (+ A <r> B) <r> B) A) # </table>
(= (.- (+ A B) B) A)
EqReplaceEq0 # <title> Substitution </title> # <table> # (= [ A ] ] ] C) # (= [ A ] [ B ] ) # (= [ [ [ B ] C) # </table>
(= A C) , (= A B)(= B C)
EqReplaceEq0Add1 # <title> Substitution </title> # <table> # (= (+ A [ B ] ] ] ) D) # (= [ B ] [ C ] ) # (= (+ A [ [ [ C ] ) D) # </table>
(= (+ A B) D) , (= B C)(= (+ A C) D)
EqReplaceImp1Eq0Add1 # <title> Substitution </title> # <table> # (-> ph (= (+ A [ B ] ] ] ) D)) # (= [ B ] [ C ] ) # (-> ph (= (+ A [ [ [ C ] ) D)) # </table>
(-> ph (= (+ A B) D)) , (= B C)(-> ph (= (+ A C) D))
halfminusaddcom # <title> Commute Half Minus </title> # <table> # (-> (<= <r> B <g> A) (= (+ (.- <g> A <r> B) <b> C) (.- (+ <g> A <b> C) <r> B))) # </table>
(-> (<= B A) (= (+ (.- A B) C) (.- (+ A C) B)))
emptyThm # <summary> This is used just for convenience to get an empty theorem. </summary>
(T)