(6steps total) PrintForm Definitions Lemmas graph 1 1 Sections Graphs Doc

At: select upto 1 1 1
1. d:
2. 0 < d
3. i,j:, k:(d-1). j-i = d-1 upto(i;j)[k] = i+k
4. i:
5. j:
6. k: d
7. j-i = d
8. i < j
9. k = 0
k||upto(i+1;j)||
By: RWO Thm* j:, i:j. ||upto(i;j)|| = j-i 0
Generated subgoals:

None

About:
intnatural_numberaddsubtractless_thanequalimpliesall

(6steps total) PrintForm Definitions Lemmas graph 1 1 Sections Graphs Doc