proposition: Lemma singleton_correct : forall b, contains (convert (singleton b)) (Xreal (proj_val (convert_bound b))).
proof: Proof. intros b. unfold singleton, convert, convert_bound. destruct F.valid_lb eqn:Hl. 2: easy. destruct F.valid_ub eqn:Hu. 2: easy. simpl. rewrite Hl, Hu. simpl. destruct F.toX. repeat split. split ; apply Rle_refl. Qed.
imports: Coq(Bool Reals Psatz) Flocq(Raux) Stdlib Xreal Basic Sig Interval