proposition: Theorem bisect_correct : forall prec n midp f fi check, (forall u v, valid f u v (fi u v)) -> valid f IBu IBv (bisect prec n midp fi check).
proof: Proof. intros prec n midp f fi check Hfi. unfold bisect. destruct check. apply Hfi. apply sum_invariant. apply iter_until_correct. intros [v p]. now apply split_piece_correct. now intros [v p]. split ; simpl. now split. exists (Piece IBu IBv (fi IBu IBv)), nil. split. apply permut_refl. easy. Qed.
imports: Coq(BinPos Reals List) Coquelicot(Coquelicot) Coquelicot Xreal Interval Priority