WellFnd{i}({...n};x,y.x > y)
;x,y.x < y) WellFnd{i}({...n};x,y.x > y)
i,j:. i > j 
-i < -j
THENC
GenLemmaWithThenLC -1 [`n',n] []
Thm* a,b,n:. a < b a+n < b+n))
-1| 1 | 3. WellFnd{i}({...n};x,y.-(n-y)+n < -(n-x)+n) WellFnd{i}({...n};x,y.x > y) |
About:
 |  |  |