Nuprl - Proof: mod plus

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

. 0<n

(

j,k:

. nmod(nmod(j;n)+nmod(k;n);n) = nmod(j+k;n))

By:

RewriteOfThm
Thm* all
Thm* (

n:hnum. implies
Thm* (

n:hnum. (lt(0,n)
Thm* (

n:hnum. ,all
Thm* (

n:hnum. ,(

j:hnum. all
Thm* (

n:hnum. ,(

j:hnum. (

k:hnum. equal
Thm* (

n:hnum. ,(

j:hnum. (

k:hnum. (mod(add(mod(j,n),mod(k,n)),n)
Thm* (

n:hnum. ,(

j:hnum. (

k:hnum. ,mod(add(j,k),n))))))
(SimpsetC [`hol_to_nuprl`;`bequal`])

Generated subgoals:

None

About:

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