Nuprl - Proof: div unique

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: div unique

, n:

, p,q:

. Div(a;n;p)

Div(a;n;q)

p = q

By:	Def of Div(<nat>;<nat>;<nat>) THEN UnivCD

Generated subgoal:

1 1. a :
2. n :
3. p :
4. q :
5. np  a < n(p+1)
6. nq  a < n(q+1)
  p = q
1 step

About:

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