k is just a notation for {0..k
}| NOTE: | k is just a notation for {0..k} |
| Who Cites int seg? | |
| int_seg | Def {i..j} == {k: | i  k < j } |
Thm*  m,n:. {m..n}  Type | |
| lelt | Def i j < k == ij & j < k |
| le | Def AB ==  B < A |
| Thm* i,j:. (ij) Prop | |
| not | Def A == A   False |
| Thm* A:Prop. (A) Prop |
| Syntax: | {i..j} | has structure: | int_seg(i; j) |
About:
 |  |  |  |  |  |
 |  |  |  |
 |