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

At: select upto 1 1 2
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
upto(i+1;j)[(k-1)] = i+k
By: InstHyp [i+1;j;k-1] 3
Generated subgoals:

None

About:
intnatural_numberaddsubtractless_thanequalimpliesall

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