fact: Fixpoint clamp_plot prec (vi ei : I.type) (h : Z) (l : list I.type) : list (Z * Z) := match l with | nil => nil | cons yi l => let r := clamp (I.mul prec (I.sub prec yi vi) ei) h in cons r (clamp_plot prec vi ei h l) end.
imports: Coq(Reals List) Sig Generic_proof Interval_helper Xreal Interval Tree Reify Prog