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

At: rem fun sat rem nrel

a:, n:. Rem(a;n;a rem n)
By:
Unfold `rem_nrel` 0
THEN
UnivCD
Generated subgoal:

11. a:
2. n:
q:. Div(a;n;q) & qn+(a rem n) = a

About:
intaddmultiplyremainderequalandallexists

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