proposition: Theorem abs_ge_0 : forall xi, not_empty (convert xi) -> convert xi <> Interval.Inan -> le_lower' (Xreal 0) (F.toX (lower (abs xi))).
proof: Proof. intros [|xl xu]. { now intros H; elim H. } intros [x Hx] _; revert Hx. unfold convert. case_eq (F.valid_lb xl); intro Vxl; [|intros [H0 H1]; lra]. case_eq (F.valid_ub xu); intro Vxu; [|intros [H0 H1]; lra]. intros [Hxl Hxu]. simpl. unfold sign_large_. rewrite 2!F.cmp_correct, F.zero_correct, F'.classify_zero. generalize Vxl Vxu. rewrite F.valid_lb_correct, F.valid_ub_correct. generalize (F.classify_correct xl) ; rewrite F.real_correct ; case_eq (F.classify xl) ; intros Cxl ; [..|easy] ; [case_eq (F.toX xl); [easy|]; intros rxl Hrxl _ _ |case_eq (F.toX xl); [|easy]; intros Hrxl _ _..] ; ( generalize (F.classify_correct xu) ; rewrite F.real_correct ; case_eq (F.classify xu) ; intros Cxu ; [..|easy|] ; [case_eq (F.toX xu); [easy|]; intros rxu Hrxu _ _ |case_eq (F.toX xu); [|easy]; intros Hrxu _ _..] ) ; unfold Xcmp ; try ( case (Rcompare_spec rxl 0) ; intros Hrxl0 ) ; try ( case (Rcompare_spec rxu 0) ; intros Hrxu0 ) ; simpl ; rewrite ?F'.neg_correct, ?F.zero_correct, ?Hrxl, ?Hrxu ; simpl ; lra. Qed.
imports: Coq(Bool Reals Psatz) Flocq(Raux) Stdlib Xreal Basic Sig Interval