# List of theorems

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

EqReplaceLe0 # <context> # This theorem is part of a series of theorems describing inequalities for # natural numbers. # </context> # <title> Substitution </title> # <table> # (<= [ A ] ] ] C) # (= [ A ] [ B ] ) # (<= [ [ [ B ] C) # </table>
(<= A C) , (= A B)(<= B C)
(<= A (+ A B))
(<= A (+ B A))
EqReplaceGt1 # <title> Substitution </title> # <table> # (> A [ B ] ] ] ) # (= [ B ] [ C ] ) # (> A [ [ [ C ] ) # </table>
(> A B) , (= B C)(> A C)
provele # <title> Addition implies ≤ </title>
(-> (= (+ A B) C) (<= A C))
(<-> (<= A B) (\/ (= A B) (<= (+ A (1)) B)))
(> (+ A (1)) A)
(<-> (< A B) (<= (+ A (1)) B))
lePlus1 # <title> Convert between ≤ and < </title> # <summary> This proves that natural numbers are whole numbers. </summary> # <suggest> right('Equivalence', '≤-1') left('Equivalence', '<') </suggest>
(<-> (< A (+ B (1))) (<= A B))
ge0 # <title> No Natural Numbers Below Zero </title>
(>= A (0))
axlttri # <title> Inequality Conversion </title> # <suggest> left('Simplify', '<') </suggest>
(<-> (< A B) (-. (\/ (= A B) (< B A))))
natWhole # <title> Natural Numbers are Whole Numbers </title>
(-. (/\ (< A B) (< B (+ A (1)))))
eq0le0 # <summary> For naturals, equal to zero is equivalent to less than or equal to zero </summary>
(<-> (= A (0)) (<= A (0)))
EqReplaceOr1Le0 # <title> Substitution </title> # <table> # (\/ ph (<= [ A ] ] ] C)) # (= [ A ] [ B ] ) # (\/ ph (<= [ [ [ B ] C)) # </table>
(\/ ph (<= A C)) , (= A B)(\/ ph (<= B C))
(\/ (= A (0)) (<= (1) A))
lemul2nat # <title> Multiply Both Sides </title> # <summary> Multiplication is monotonic in its second argument </summary>
(-> (<= A B) (<= (* C A) (* C B)))
ltle2 # <title> Convert between ≤ and < </title> # <suggest> right('Equivalence', '≤+1') left('Equivalence', '<-1') </suggest>
(<-> (< A B) (<= (+ A (1)) B))