(3steps) PrintForm Definitions Lemmas int 2 Sections StandardLIB Doc

At: minus functionality wrt le 1 1

1. i:
2. j:
3. ji

-i-j

By: RA ((Assert (-(i+j)-(i+j))) THEN (FwdThru Thm* i1,i2,j1,j2:. i1j1 i2j2 i1+i2j1+j2 [3;-1]))

Generated subgoals:

None


About:
intminusadd

(3steps) PrintForm Definitions Lemmas int 2 Sections StandardLIB Doc