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