IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
hndiv unique all
(n:hnum. all
(n:hnum. (k:hnum. all
(n:hnum. (k:hnum. (q:hnum. implies
(n:hnum. (k:hnum. (q:hnum. (exists
(n:hnum. (k:hnum. (q:hnum. ((r:hnum. and
(n:hnum. (k:hnum. (q:hnum. ((r:hnum. (equal(k,add(mult(q,n),r))
(n:hnum. (k:hnum. (q:hnum. ((r:hnum. ,lt(r,n)))
(n:hnum. (k:hnum. (q:hnum. ,equal(div(k,n),q)))))
By:
HOL "hndiv_unique"
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
all
(
n:hnum. all
