IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
rem 3 to 1 a:{...0}, n:{...-1}. (a rem n) = -((-a) rem -n)
By:
Auto THEN Rewrite by Thm*a:, b:. ((-a) rem b) = -(a rem b)
THEN
Rewrite by Thm*a:, b:. (a rem -b) = (a rem b)
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
a:{...0}, n:{...-1}. (a rem n) = -((-a) rem -n)
, b:
. ((-a) rem b) = -(a rem b)
