Nuprl - Proof: div lbound 1 1 2

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

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: div lbound 1 1 2

1. a :

2. n :

3. k :

4. a = (a

n)

n+(a rem n)
5. (a rem n)

n
6. k

n

a

k

(a

n)

By:	FwdThru: Thm* k:, r1,r2:k, q1,q2:. q1k+r1q2k+r2 q1q2 on [ kn+0(a n)n+(a rem n) ]

Generated subgoals:

None

About:

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

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