proposition: Theorem neg_correct : extension Xneg neg.
proof: Proof. intros [ | xl xu] [ | x] ; simpl ; trivial; [now case (_ && _)|]. case_eq (F.valid_lb xl); [|intros _ [H0 H1]; exfalso; lra]. case_eq (F.valid_ub xu); [|intros _ _ [H0 H1]; exfalso; lra]. intros Vu Vl (Hxl, Hxu). rewrite F'.valid_lb_neg, F'.valid_ub_neg, Vu, Vl. rewrite !F'.neg_correct. now split ; [ xreal_tac xu | xreal_tac xl ] ; apply Ropp_le_contravar. Qed.
imports: Coq(Bool Reals Psatz) Flocq(Raux) Stdlib Xreal Basic Sig Interval