Issue:
For taylor sine degree 3

E1 = model error
E2 = rounding error
E3 = fp-taylor cushion
E4 = lppaver cushion

E1 + E2 + E3 = 0.00025888789504748890456219
https://www.wolframalpha.com/input?i=0.00025887019991748890456219+%2B+0.00000001769513

But I can verify with 0.00025886, E4 is negative?
Noticed that
0.00025886 > E1 - (E2 + E3)
0.00025886 > 0.00025885250478748890456219
https://www.wolframalpha.com/input?i=0.00025887019991748890456219+-+0.00000001769513

0.00025885 gives sat

Theory: direction of elimination of floats is incorrect, but why?

I want to prove a contradiction.

f1 and f2 contain some fp ops
r1 and r2 are bounds from FPTaylor for f1 and f2
e1 and e2 is f1 and f2 without fp ops

currently, we would eliminate floats by strengthening, and then negate everything

f1 < f2

floats eliminated by strengthening formula. We get:

e1 + r1 < e2 - r2

We then negate everything:

! (e1 + r1 < e2 - r2)
e1 + r1 >= e2 - r2

We are *weakening* the contradiction which is unsafe? We should strengthen the contradiction

I think we should do one of the following:

If we not before elim, we get:

f1 < f2

f1 >= f2

eliminate floats by strengthening

e1 - r1 >= e2 + r2

OR

f1 < f2
elimiante floats by weakening
e1 - r1 < e2 + r2

then negate everything

e1 - r1 >= e2 + r2