proposition: Theorem bisect_correct : forall xi x, contains (convert xi) x -> contains (convert (fst (bisect xi))) x \/ contains (convert (snd (bisect xi))) x.
proof: Proof. intros xi x Hx. destruct (midpoint_correct xi) as [H1 H2]. { apply not_empty_contains with (1 := Hx). } unfold bisect. set (m := midpoint xi). fold m in H1, H2. clearbody m. destruct xi as [|xl xu]. now left. revert Hx. simpl. destruct x as [|x]. now case (_ && _). destruct (F.valid_lb xl). 2: simpl ; lra. destruct (F.valid_ub xu). 2: simpl ; lra. intros [H3 H4]. rewrite valid_lb_real by easy. rewrite valid_ub_real by easy. simpl. rewrite H1. destruct (Rle_or_lt x (proj_val (F.toX m))) as [H5|H5]. now left. right. split. now apply Rlt_le. exact H4. Qed.
imports: Coq(Bool Reals Psatz) Flocq(Raux) Stdlib Xreal Basic Sig Interval