proposition: Theorem neg_correct' : forall xi x, contains (convert (neg xi)) (Xneg x) -> contains (convert xi) x.
proof: Proof. intros [|xl xu] [|x] ; try easy ; unfold convert ; simpl ; rewrite F'.valid_lb_neg, F'.valid_ub_neg, !F'.neg_correct ; [now case (_ && _)|]. rewrite andb_comm; case (_ && _); [|simpl; lra]. destruct (F.toX xl) as [|xl'] ; destruct (F.toX xu) as [|xu'] ; simpl. easy. intros [H _]. apply (conj I). now apply Ropp_le_cancel. intros [_ H]. refine (conj _ I). now apply Ropp_le_cancel. intros [H1 H2]. now split ; apply Ropp_le_cancel. Qed.
imports: Coq(Bool Reals Psatz) Flocq(Raux) Stdlib Xreal Basic Sig Interval