proposition: Theorem lower_complement_correct : forall xi x y, contains (convert xi) (Xreal x) -> contains (convert (lower_complement xi)) (Xreal y) -> (y <= x)%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 xl). intros _ H'. now apply empty_correct in H'. intros l Hl. unfold convert. rewrite F'.valid_lb_nan; simpl. case F.valid_ub; [|simpl; lra]. intros [_ H']. rewrite Hl in H, H'. now apply Rle_trans with l. Qed.
imports: Coq(Bool Reals Psatz) Flocq(Raux) Stdlib Xreal Basic Sig Interval