The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

Is there a version of omega that includes min and max?  I know one could 
write a tactic that uses lt_dec to case-analyze away all mins and maxes 
- I am just wondering if this has already been done - or, perhaps even 
something more efficient that wouldn't bother to explore the entire space.

-- Jonathan