Def P  Q == (P  Q) & (P  Q)

is mentioned by

Thm* m,n:. m+1<n+1  m<n

[less_mono_eq]

In prior sections: core

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