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

At: no repeats upto 1 2 1 1
1. d:
2. 0 < d
3. i,j:. j-i = d-1 no_repeats(;upto(i;j))
4. i:
5. j:
6. j-i = d
7. i < j
(i upto(i+1;j))
By:
Analyze 0
THEN
RWO Thm* i,j,k:. (k upto(i;j)) ik & k < j -1
Generated subgoals:

None

About:
intnatural_numberaddsubtractless_thanequalimpliesandall

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