| Some definitions of interest. |
|
le_int | Def ij == j<i |
| | Thm* i,j:. (ij) |
|
bnot | Def b == if b false else true fi |
| | Thm* b:. b |
|
eq_int | Def i=j == if i=j true ; false fi |
| | Thm* i,j:. (i=j) |
|
int_iseg | Def {i...j} == {k:| ik & kj } |
| | Thm* i,j:. {i...j} Type |
|
int_nzero | Def == {i:| i 0 } |
| | Thm* Type |
|
int_seg | Def {i..j} == {k:| i k < j } |
| | Thm* m,n:. {m..n} Type |
|
lelt | Def i j < k == ij & j<k |
|
nat | Def == {i:| 0i } |
| | Thm* Type |
|
le | Def AB == B<A |
| | Thm* i,j:. (ij) Prop |
|
lt_int | Def i<j == if i<j true ; false fi |
| | Thm* i,j:. (i<j) |
|
nat_plus | Def == {i:| 0<i } |
| | Thm* Type |
|
nequal | Def a b T == a = b T |
| | Thm* A:Type, x,y:A. (x y) Prop |