proposition: Lemma upper_correct : forall xi : type, not_empty (convert xi) -> F.toX (upper xi) = Xupper (convert xi).
proof: Proof. intros [|xl xu]. simpl. now rewrite F'.nan_correct. simpl; unfold convert; case (_ && _); [easy|]. intros [x Hx]; revert Hx; simpl; lra. Qed.
imports: Coq(Bool Reals Psatz) Flocq(Raux) Stdlib Xreal Basic Sig Interval