In src/coqapprox:
- Rename not_empty'E as not_emptyE & Define not_empty'E as the converse result
- Move the PolyMap functor into taylor_model_int_sharp.v
- Add several support lemmas in taylor_model_int_sharp.v
- Define a predicate is_const
- Formalize two functions TM_mul_mixed/TM_div_mixed_r
In src:
- Replace TM_const with TM_cst whenever possible, as it yields tighter bounds
- Update TM.mul/TM.div to compute (Const * Tm) or (Tm / Const) more efficiently
- Update Interval_taylor_model's proofs accordingly
- Note that no change has been done in Interval_univariate's interface
In testsuite:
- While the perfs of TM.const/TM.mul/TM.div are increased, for the Rabs example
  we'd rather use "interval with (i_depth 0, i_prec 0)" or add a small epsilon.