is mentioned by

Thm*  b,a:. b(b -- a)+a	[ndiff_bound]
Thm*  a,b:. ab  (b -- a) = b-a	[ndiff_vs_diff]

In prior sections: int 2

Try larger context: DiscrMathExt IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html