proposition: Lemma contains_only_0 r : contains (I.convert I.zero) (Xreal r) -> r = 0%R.
proof: Proof. rewrite I.zero_correct. intros [H1 H2]. now apply Rle_antisym. Qed.
imports: Coq(Bool Reals Psatz) Coquelicot(Coquelicot) Stdlib Xreal Basic