IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
hmod plus all
(n:hnum. implies
(n:hnum. (lt(0,n)
(n:hnum. ,all
(n:hnum. ,(j:hnum. all
(n:hnum. ,(j:hnum. (k:hnum. equal
(n:hnum. ,(j:hnum. (k:hnum. (mod(add(mod(j,n),mod(k,n)),n)
(n:hnum. ,(j:hnum. (k:hnum. ,mod(add(j,k),n))))))
By:
HOL "hmod_plus"
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html