IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
The proof here illustrates how the evaluation of the extract of one theorem (decidable__divides) can help to prove another theorem.
For neatness, the pattern of proof here could easily be incorporated into a tactic.
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html