PrintForm Definitions Lemmas int 2 Sections StandardLIB Search Doc
IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: rem bounds 1 typing sfa

  a:n:. (a rem n n

By: UnivCD THEN Inst: Thm* a:n:. 0(a rem n) & (a rem n)<n Using:[a | n]


Generated subgoals:

None

About:
natural_numberremainderless_thanmemberandall
IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html

PrintForm Definitions Lemmas int 2 Sections StandardLIB Search Doc