proposition: Theorem upper_extent_correct : forall xi x y, contains (convert xi) (Xreal y) -> (y <= x)%R -> contains (convert (upper_extent xi)) (Xreal x).
proof: Proof. assert (H1v0 : forall v, ~(1 <= v <= 0)%R). { intros v Hf. apply (Rlt_irrefl 0), (Rlt_le_trans _ 1); [apply Rlt_0_1|]. elim Hf; apply Rle_trans. } intros [|xl xu] x y; simpl; [now simpl|]. case_eq (F.valid_lb xl); intro Vxl; [|now intro H; destruct (H1v0 y)]. case_eq (F.valid_ub xu); intro Vxu; [|now intro H; destruct (H1v0 y)]. intros (Hxl, Hxu) Hx; rewrite F'.valid_ub_nan; split. { now revert Hxl; xreal_tac xl; [now simpl|]; intro Hxl; apply (Rle_trans _ y). } now rewrite F'.nan_correct. Qed.
imports: Coq(Bool Reals Psatz) Flocq(Raux) Stdlib Xreal Basic Sig Interval