Nuprl - Proof: divides iff div exact

IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: divides iff div exact

, n:

. n | a

n = a

By:

GenUnivCD

Generated subgoals:

1 1. a :
2. n :
3. n | a
  (a  n)n = a
4 steps

2 1. a :
2. n :
3. (a  n)n = a
  n | a
2 steps

About:

IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html

1	1. a : 2. n : 3. n \| a (a n)n = a	4 steps
2	1. a : 2. n : 3. (a n)n = a n \| a	2 steps