Add requirements of TotalEq and TotalOrd

Add requirements of TotalEq and TotalOrd

Clarify that TotalEq needs an underlying equivalence relation and that TotalOrd
needs a total ordering and specifically named the required (and sufficient)
attributes.