fact: Definition split_piece prec midp fi sp := let le_piece := le_piece prec in match sp with | (s, p) => match ptree_pop le_piece p with | (Piece u v i, h) => let m := IBp (midp u v) in let i1 := fi u m in let i2 := fi m v in let p1 := Piece u m i1 in let p2 := Piece m v i2 in let s := I.add prec (I.cancel_add prec s i) (I.add prec i1 i2) in let p := ptree_insert le_piece (pheap_insert le_piece h p1) p2 in (s, p) end end.
imports: Coq(BinPos Reals List) Coquelicot(Coquelicot) Coquelicot Xreal Interval Priority