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

At: no repeats upto 2 2
1. d,i,j:. j-i = d no_repeats(;upto(i;j))
2. i:
3. j:
4. ij
no_repeats(;upto(i;j))
By:
RecUnfold `upto` 0
THEN
SplitOnConclITE
Generated subgoal:

15. ji
no_repeats(;nil)		1 step

About:
nilintsubtractequalimpliesall

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