Nuprl - Proof: mod times

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: mod times

. 0<n

(

q,r:

. nmod(q

n+r;n) = nmod(r;n))

By:	RewriteOfThm Thm* all Thm* (n:hnum. implies Thm* (n:hnum. (lt(0,n) Thm* (n:hnum. ,all Thm* (n:hnum. ,(q:hnum. all Thm* (n:hnum. ,(q:hnum. (r:hnum. equal(mod(add(mult(q,n),r),n),mod(r,n)))))) (SimpsetC [`hol_to_nuprl`;`bequal`])

Generated subgoals:

None

About:

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