Add lower bound lemma for finite sets

Forked off from the discussion here: lambda-rust!38 (comment 104108)

This adds a variant of minimal_exists which does not require the set to be non-empty, but in return also does not guarantee that the element is part of the set.

I'm not sure what the best naming for this lemma is. Maybe it should be called infimum_exists instead of lower_bound_exists? Should it be prefixed by set, like many other lemmas in the file for which it is not directly clear it's related to sets? (and should minimal_exists be prefixed accordingly?)