∀ (date : Std.Time.PlainDate) (desiredWeekday : Std.Time.Weekday),
  ↑(Std.Time.Internal.Bounded.LE.subBounds desiredWeekday.toOrdinal date.weekday.toOrdinal) < 0 →
    ↑(Std.Time.Internal.Bounded.LE.subBounds desiredWeekday.toOrdinal date.weekday.toOrdinal) ≤ 0 - 1