(4steps total) PrintForm Definitions graph 1 1 Sections Graphs Doc

At: length upto 1 1
1. d:
2. 0 < d
3. j,i:. j-i = d-1 ||upto(i;j)|| = d-1
4. j:
5. i:
6. j-i = d
7. i < j
||upto(i+1;j)||+1 = d
By: InstHyp [j;i+1] 3
Generated subgoals:

None

About:
intnatural_numberaddsubtractless_thanequalimpliesall

(4steps total) PrintForm Definitions graph 1 1 Sections Graphs Doc