proposition: Theorem upper_complement_correct : forall xi x y, contains (convert xi) (Xreal x) -> contains (convert (upper_complement xi)) (Xreal y) -> (x <= y)%R.
proof: Proof. intros [|xl xu] x y. intros _ H. now apply empty_correct in H. unfold convert at 1. case F.valid_lb; simpl; [|lra]. case F.valid_ub; simpl; [|lra]. intros [_ H]. simpl. rewrite F.real_correct. case_eq (F.toX xu). intros _ H'. now apply empty_correct in H'. intros u Hu. unfold convert. rewrite F'.valid_ub_nan; simpl. case F.valid_lb; [|simpl; lra]. intros [H' _]. rewrite Hu in H, H'. now apply Rle_trans with u. Qed.
imports: Coq(Bool Reals Psatz) Flocq(Raux) Stdlib Xreal Basic Sig Interval