proposition: Theorem upper_bounded_correct : forall xi, upper_bounded xi = true -> F.toX (upper xi) = Xreal (proj_val (F.toX (upper xi))) /\ bounded_prop xi.
proof: Proof. unfold upper_bounded. intros [|xl xu] H. discriminate H. generalize (F.real_correct xu). rewrite H. clear H. simpl. unfold F.toX. case (F.toF xu). intro H. discriminate H. repeat split. { unfold bounded_prop, convert; simpl; case (_ && _); [easy|]. intros [x Hx]; revert Hx; simpl; lra. } intros s m e; case (FtoX _); [now simpl|]; intros r _; split; [now simpl|]. unfold bounded_prop, convert; simpl; case (_ && _); [easy|]. intros [x Hx]; revert Hx; simpl; lra. Qed.
imports: Coq(Bool Reals Psatz) Flocq(Raux) Stdlib Xreal Basic Sig Interval