proposition: Lemma ComputeBound_propagate : forall prec pi, J.propagate (ComputeBound prec pi).
proof: Proof. red=> *; rewrite /ComputeBound /=. by repeat match goal with [|- context [if ?b then _ else _]] => destruct b end; rewrite !(I.add_propagate_r,I.mul_propagate_l,J.power_int_propagate, Pol.horner_propagate). Qed.
imports: Coq(ZArith Reals) Flocq(Raux) mathcomp.ssreflect(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype bigop) Xreal Interval MathComp Datatypes Bound