proposition: Lemma bnd_correct : forall l u, valid_lb l -> valid_ub u -> convert (bnd l u) = Interval.Ibnd (F.toX l) (F.toX u).
proof: Proof. now intros l u Vl Vu; unfold convert; simpl; rewrite Vl, Vu. Qed.
imports: Coq(Bool Reals Psatz) Flocq(Raux) Stdlib Xreal Basic Sig Interval