Added x≤y→x-y≡0 (by Ana Bove).
Added x≤y→x-y≡0 (by Ana Bove).

Ignore-this: fa2d051e8f718179b58746fc80b2a0dd

darcs-hash:20110210164711-3bd4e-262b0518a2141dda47047d0d64406b023ca59c1f.gz

asr/fotc,asr/fotc