high-level plugs done, using a postulate that relates >= and <=