(
n,k:
. (n r k) 
Min{ x | xrn } = Min{ x | xrk }) & (n:. n r Min{ x | xrn })
Propx,y:. Dec(x E y)
x,y:. (x r y) (x E y). x r y (n,k:. (n r k) Min{ x | xrn } = Min{ x | xrk }) & (n:. n r Min{ x | xrn })| 1 | (n,k:. (n r k) Min{ x | xrn } = Min{ x | xrk }) & (n:. n r Min{ x | xrn }) |
About:
 |  |  |  |  |  |  |