fact: Definition sum prec (p : ptree piece) := ptree_fold (fun acc v => I.add prec acc match v with Piece _ _ i => i end) p I.zero.
imports: Coq(BinPos Reals List) Coquelicot(Coquelicot) Coquelicot Xreal Interval Priority