Nuprl - Proof: rem antisym 1 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

1. a :

2. b :

3. 0

a
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)

By:	FwdThru: Thm* k:, r1,r2:k, q1,q2:. q1k+r1 = q2k+r2 q1 = q2 & r1 = r2 on [ (-((-a) b))b+-((-a) rem b) = (a b)b+(a rem b) ]

Generated subgoals:

None

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