fact: Fixpoint bound_plot_aux prec (fi : I.type -> I.type) (ui di : I.type) (xz : Z) (i : nat) (acc : I.type) : I.type := match i with | O => acc | S i => let xz := Z.succ xz in let xi := I.add prec ui (I.mul prec di (I.fromZ prec xz)) in bound_plot_aux prec fi ui di xz i (I.join (fi xi) acc) end.
imports: Coq(Reals List) Sig Generic_proof Interval_helper Xreal Interval Tree Reify Prog