Nuprl - Proof: rem fun sat rem nrel

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: rem fun sat rem nrel

, n:

. Rem(a;n;a rem n)

By:	Def of Rem(<nat>;<nat>;<nat>)

Generated subgoal:

1 a:, n:. q:. Div(a;n;q) & qn+(a rem n) = a
3 steps

About:

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html