proposition: Theorem abs_ge_0' : forall xi, not_empty (convert xi) -> (0 <= proj_val (F.toX (lower (abs xi))))%R.
proof: Proof. intros [|xl xu] Hne. simpl. rewrite F'.nan_correct. apply Rle_refl. refine (_ (abs_ge_0 (Ibnd xl xu) Hne _)). 2: now unfold convert; case (_ && _). simpl. now case F.toX. Qed.
imports: Coq(Bool Reals Psatz) Flocq(Raux) Stdlib Xreal Basic Sig Interval