feat: add lower/upper approximant theory (1/?)

[bollu]

Now, I'm showing that functions called lower and upper exist. Recall that they are currently given axiomatically, but to show equivalence to the circuit, we need a more computational definition. This will be a (long) line of technical lemmas:

1. All packed floats that are numbers are larger than minSubnorm, smaller than maxNorm.
2. If you are smaller than minSubnorm, then you are zero. If you are larger than maxNorm, then you are infinity.
3. for every ExtRat, there will either be a PackedFloat smaller than it, or itis equal to a packed float (similar for upper)
4. Between any two PackedFloats, there is a finite number of PackedFloats between them (from the gap theorem). This one is a bit tricky, I'm not quite sure what the "good" statement of this theorem is. I may just exhibit that the PackedFloats are finite, and can be put into an ordered list for the non-NaN fragment, which immediately gives you the ordering theorems. On paper, stuff that follows from finiteness is "immediate", but I'm not sure what the best way to express this in a proof assistant. Maybe @Léo Stefanesco , @Henrik Böving , @Abdalrhman M Mohamed have thoughts.
5. Therefore, there must exist a greatest lower bound, since (1) a lower bound exists, and (2) the set of lower bounds is finite (as it is a subset of the full universe of packed floats.)
6. Mutatis Mutandis for upper bounds.