Definition boundsYOrder (b : boundsT) : Prop :=
  (boundsYMinimum b) <= (boundsYMaximum b).
