Nuprl - Proof: div lbound 1 1 1

(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 1

1. a :

2. n :

3. k :

4. a = (a

n)

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

n
6. k

(a

n)

k

n

a

By:	FwdThru: Thm* a,b:, n:. ab nanb on [ k(a n) ] Using:[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