| | Some definitions of interest. |
|
| le_int | Def i  j ==  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 |
