| Some definitions of interest. |
|
coprime | Def CoPrime(a,b) == GCD(a;b;1) |
| | Thm* a,b:. CoPrime(a,b) Prop |
|
eqmod | Def a = b mod m == m | a-b |
| | Thm* m,a,b:. (a = b mod m) Prop |
|
divides | Def b | a == c:. a = bc |
| | Thm* a,b:. (a | b) Prop |
|
nat_plus | Def == {i:| 0<i } |
| | Thm* Type |