Nuprl - Proof: mod mult

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

n,r:

. r<n

(

. nmod(q

n+r;n) = r)

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

Generated subgoals:

None

About:

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