proposition: Lemma valid_ub_upper : forall xi : type, not_empty (convert xi) -> valid_ub (upper xi).
proof: Proof. intros [|l u] [x Hx]; unfold valid_ub; simpl; [now rewrite F'.valid_ub_nan|]. revert Hx; unfold convert. now case F.valid_ub; rewrite andb_comm; [|simpl; lra]. Qed.
imports: Coq(Bool Reals Psatz) Flocq(Raux) Stdlib Xreal Basic Sig Interval