List of theorems

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

BiReplaceImp1Ex1 # <context> # This theorem is part of a series of theorems demonstrating that it is possible # to cancel an nonzero number from both sides of an equation. It is assumed that # every number in this theorem is a natural number. # </context> # <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))
sucmulcan # <summary> Multiplication cancellation with nonzero multiplicand </summary>
(<-> (= (* A (+ C (1))) (* B (+ C (1)))) (= A B))
EqReplaceImp1Ex1Eq0 # <title> Substitution </title> # <table> # (-> ph (E. x (= [ A ] ] ] C))) # (= [ A ] [ B ] ) # (-> ph (E. x (= [ [ [ B ] C))) # </table>
(-> ph (E. x (= A C))) , (= A B)(-> ph (E. x (= B C)))
mulcan # <title> Cancel Multiplication </title>
(-> (-. (= C (0))) (<-> (= (* A C) (* B C)) (= A B)))