proposition: Lemma ComputeBound_propagate : forall prec pi, J.propagate (ComputeBound prec pi).
proof: Proof. by red=> *; rewrite /ComputeBound Pol.horner_propagate. Qed.
imports: Coq(ZArith Reals Psatz) mathcomp.ssreflect(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype bigop) Interval MathComp Datatypes