Nuprl - Pf remainder_wf 1 1

(5steps) PrintForm Definitions Lemmas int 2 Sections StandardLIB Doc

At: remainder wf 1 1

1. a:
2. n:

(a rem n) = (a rem n)

By: PrimEqCD

Generated subgoals:

None

About:

(5steps) PrintForm Definitions Lemmas int 2 Sections StandardLIB Doc