3 `m + (SUC n) = SUC(m + n)`;
5 `m + (n + p) = (m + n) + p`;
6 `(m + n) + p = m + (n + p)`;
7 `(m + n = 0) <=> (m = 0) /\ (n = 0)`;
8 `(m + n = m + p) <=> (n = p)`;
9 `(m + p = n + p) <=> (m = n)`;
10 `(m + n = m) <=> (n = 0)`;
11 `(m + n = n) <=> (m = 0)`;
14 `m * (SUC n) = m + (m * n)`;
15 `(0 * n = 0) /\ (m * 0 = 0) /\ (1 * n = n) /\ (m * 1 = m) /\ ((SUC m) * n = (m * n) + n) /\ (m * (SUC n) = m + (m * n))`;
17 `m * (n + p) = (m * n) + (m * p)`;
18 `(m + n) * p = (m * p) + (n * p)`;
19 `m * (n * p) = (m * n) * p`;
20 `(m * n = 0) <=> (m = 0) \/ (n = 0)`;
21 `(m * n = m * p) <=> (m = 0) \/ (n = p)`;
22 `(m * p = n * p) <=> (m = n) \/ (p = 0)`;
23 `SUC(SUC(0)) * n = n + n`;
24 `(m * n = SUC(0)) <=> (m = SUC(0)) /\ (n = SUC(0))`;
25 `(m EXP n = 0) <=> (m = 0) /\ ~(n = 0)`;
26 `m EXP (n + p) = (m EXP n) * (m EXP p)`;
27 `SUC(0) EXP n = SUC(0)`;
29 `n EXP SUC(SUC(0)) = n * n`;
30 `(m * n) EXP p = m EXP p * n EXP p`;
31 `m EXP (n * p) = (m EXP n) EXP p`;
32 `(SUC m <= n) <=> (m < n)`;
33 `(m < SUC n) <=> (m <= n)`;
34 `(SUC m <= SUC n) <=> (m <= n)`;
35 `(SUC m < SUC n) <=> (m < n)`;
40 `(m <= n /\ n <= m) <=> (m = n)`;
44 `m <= n /\ n <= p ==> m <= p`;
45 `m < n /\ n < p ==> m < p`;
46 `m <= n /\ n < p ==> m < p`;
47 `m < n /\ n <= p ==> m < p`;
49 `(m < n) \/ (n < m) \/ (m = n)`;
53 `(m <= n) <=> (m < n) \/ (m = n)`;
54 `(m < n) <=> (m <= n) /\ ~(m = n)`;
55 `~(m <= n) <=> (n < m)`;
56 `~(m < n) <=> n <= m`;
61 `(m < m + n) <=> (0 < n)`;
62 `(n < m + n) <=> (0 < m)`;
63 `(m + n) <= (m + p) <=> n <= p`;
64 `(m + p) <= (n + p) <=> (m <= n)`;
65 `(m + n) < (m + p) <=> n < p`;
66 `(m + p) < (n + p) <=> (m < n)`;
67 `m <= p /\ n <= q ==> m + n <= p + q`;
68 `m <= p /\ n < q ==> m + n < p + q`;
69 `m < p /\ n <= q ==> m + n < p + q`;
70 `m < p /\ n < q ==> m + n < p + q`;
71 `(0 < m * n) <=> (0 < m) /\ (0 < n)`;
72 `m <= n /\ p <= q ==> m * p <= n * q`;
73 `~(m = 0) /\ n < p ==> m * n < m * p`;
74 `(m * n) <= (m * p) <=> (m = 0) \/ n <= p`;
75 `(m * p) <= (n * p) <=> (m <= n) \/ (p = 0)`;
76 `(m * n) < (m * p) <=> ~(m = 0) /\ n < p`;
77 `(m * p) < (n * p) <=> (m < n) /\ ~(p = 0)`;
78 `(SUC m = SUC n) <=> (m = n)`;
79 `m < n /\ p < q ==> m * p < n * q`;
81 `(P m n <=> P n m) /\ (m <= n ==> P m n) ==> P m n`;
82 `(P m m) /\ (P m n <=> P n m) /\ (m < n ==> P m n) ==> P m y`;
83 `((m < n ==> P m) ==> P n) ==> P n`;
84 `~(EVEN n) <=> ODD n`;
85 `~(ODD n) <=> EVEN n`;
88 `EVEN(m + n) <=> (EVEN m <=> EVEN n)`;
89 `EVEN(m * n) <=> EVEN(m) \/ EVEN(n)`;
90 `EVEN(m EXP n) <=> EVEN(m) /\ ~(n = 0)`;
91 `ODD(m + n) <=> ~(ODD m <=> ODD n)`;
92 `ODD(m * n) <=> ODD(m) /\ ODD(n)`;
93 `ODD(m EXP n) <=> ODD(m) \/ (n = 0)`;
94 `EVEN(SUC(SUC(0)) * n)`;
95 `ODD(SUC(SUC(SUC(0)) * n))`;
96 `(0 - m = 0) /\ (m - 0 = m)`;
97 `PRE(SUC m - n) = m - n`;
98 `SUC m - SUC n = m - n`;
102 `(m - n = 0) <=> m <= n`;
105 `n <= m ==> ((m - n) + n = m)`;
106 `(m + n) - (m + p) = n - p`;
107 `(m + p) - (n + p) = m - n`;
108 `m * (n - p) = m * n - m * p`;
109 `(m - n) * p = m * p - n * p`;
110 `!n. SUC n - SUC(0) = n`;
111 `EVEN(m - n) <=> m <= n \/ (EVEN(m) <=> EVEN(n))`;
112 `ODD(m - n) <=> n < m /\ ~(ODD m <=> ODD n)`;
115 `m <= n ==> FACT m <= FACT n`;
116 `0 < x EXP n <=> ~(x = 0) \/ (n = 0)`;
117 `x EXP m < x EXP n <=> SUC(SUC(0)) <= x /\ m < n \/ (x = 0) /\ ~(m = 0) /\ (n = 0)`;
118 `x EXP m <= x EXP n <=> if x = 0 then (m = 0) ==> (n = 0) else (x = 1) \/ m <= n`;
119 `~(p = 0) /\ m <= n ==> m DIV p <= n DIV p`;
120 `P(PRE n) <=> n = SUC m \/ m = 0 /\ n = 0 ==> P m`