# List of theorems

List of theorems in peano_new/arithmetic/common/calculations/integers.gh:

EqReplaceEq1Neg0 # <title> Substitution </title> # <table> # (= A (-n [ B ] ] ] )) # (= [ B ] [ C ] ) # (= A (-n [ [ [ C ] )) # </table>
(= A (-n B)) , (= B C)(= A (-n C))
(= (* (-n (3)) (4)) (-n (+ (10) (2))))
EqReplaceEq1Add1 # <title> Substitution </title> # <table> # (= A (+ B [ C ] ] ] )) # (= [ C ] [ D ] ) # (= A (+ B [ [ [ D ] )) # </table>
(= A (+ B C)) , (= C D)(= A (+ B D))
EqReplaceEq1Add0 # <title> Substitution </title> # <table> # (= A (+ [ B ] ] ] D)) # (= [ B ] [ C ] ) # (= A (+ [ [ [ C ] D)) # </table>
(= A (+ B D)) , (= B C)(= A (+ C D))
EqReplaceEq1Add0Mul0 # <title> Substitution </title> # <table> # (= A (+ (* [ B ] ] ] D) A')) # (= [ B ] [ C ] ) # (= A (+ (* [ [ [ C ] D) A')) # </table>
(= A (+ (* B D) A')) , (= B C)(= A (+ (* C D) A'))
EqReplaceEq1Add0Add1 # <title> Substitution </title> # <table> # (= A (+ (+ B [ C ] ] ] ) A')) # (= [ C ] [ D ] ) # (= A (+ (+ B [ [ [ D ] ) A')) # </table>
(= A (+ (+ B C) A')) , (= C D)(= A (+ (+ B D) A'))
EqReplaceEq1Add0Add1Mul0 # <title> Substitution </title> # <table> # (= A (+ (+ B (* [ C ] ] ] A')) B')) # (= [ C ] [ D ] ) # (= A (+ (+ B (* [ [ [ D ] A')) B')) # </table>
(= A (+ (+ B (* C A')) B')) , (= C D)(= A (+ (+ B (* D A')) B'))
EqReplaceEq1Add0Add0 # <title> Substitution </title> # <table> # (= A (+ (+ [ B ] ] ] D) A')) # (= [ B ] [ C ] ) # (= A (+ (+ [ [ [ C ] D) A')) # </table>
(= A (+ (+ B D) A')) , (= B C)(= A (+ (+ C D) A'))
EqReplaceEq1Add0Add0Mul0 # <title> Substitution </title> # <table> # (= A (+ (+ (* [ B ] ] ] D) A') B')) # (= [ B ] [ C ] ) # (= A (+ (+ (* [ [ [ C ] D) A') B')) # </table>
(= A (+ (+ (* B D) A') B')) , (= B C)(= A (+ (+ (* C D) A') B'))
(= (* (-n (+ (10) (3))) (-n (+ (10) (7)))) (+ (* (2) (* (10) (10))) (+ (* (2) (10)) (1))))
emptyThm # <summary> This is used just for convenience to get an empty theorem. </summary>
(T)