Nuprl - Pf rem_invariant 1 1

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

At: rem invariant 1 1

1. a:
2. n:

((a+0n) rem n) = (a rem n)

By: Auto

Generated subgoals:

None

About:

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