Nuprl - Proof: rem antisym 1

(7steps total) PrintForm Definitions Lemmas int 2 Sections StandardLIB Doc

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: rem antisym 1

1. a :

2. b :

((-a) rem b) = -(a rem b)

By:	Decide: 0a THEN ElaborateDivision Auto 0

Generated subgoals:

1 3. 0a
4. -a = ((-a)  b)b+((-a) rem b)
5. a = (a  b)b+(a rem b)
6. -((-a) rem b)  b
7. (a rem b)  b
  ((-a) rem b) = -(a rem b)
1 step

2 3. 0a
4. -a = ((-a)  b)b+((-a) rem b)
5. a = (a  b)b+(a rem b)
6. ((-a) rem b)  b
7. -(a rem b)  b
  ((-a) rem b) = -(a rem b)
1 step

About:

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

(7steps total) PrintForm Definitions Lemmas int 2 Sections StandardLIB Doc

1	3. 0a 4. -a = ((-a) b)b+((-a) rem b) 5. a = (a b)b+(a rem b) 6. -((-a) rem b) b 7. (a rem b) b ((-a) rem b) = -(a rem b)	1 step
2	3. 0a 4. -a = ((-a) b)b+((-a) rem b) 5. a = (a b)b+(a rem b) 6. ((-a) rem b) b 7. -(a rem b) b ((-a) rem b) = -(a rem b)	1 step