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

At: no repeats upto 1
d,i,j:. j-i = d no_repeats(;upto(i;j))
By: InductionOnNat
Generated subgoals:

1 i,j:. j-i = 0 no_repeats(;upto(i;j))2 steps
 
21. d:
2. 0 < d
3. i,j:. j-i = d-1 no_repeats(;upto(i;j))
i,j:. j-i = d no_repeats(;upto(i;j))		3 steps

About:
intnatural_numbersubtractequalimpliesall

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