Improve and fix secant and tangent lemmas in the transcendental solver (#4689)

Improve and fix secant and tangent lemmas in the transcendental solver (#4689)

Fixes #4686.

This benchmark failed an assertion that corresponded to the fact that a refinement lemma did not evaluate to false in the current model (and hence does not rule out the current model).

This was caused by applying the rewriter in a way that led to an incorrect approximation. This meant that some tangent and secant lemmas would be ineffective.

The benchmark in that issue now times out, but makes progress in the refinement lemmas it generates.

This also simplifies and improves the use of approximated values (instead of model values) when constructing tangent and secant lemmas.