proposition: Theorem add_correct : forall prec, extension_2 Xadd (add prec).
proof: Proof. intros prec [ | xl xu] [ | yl yu] [ | x] [ | y] ; trivial; [| |intros _|]; [now unfold convert; case (_ && _)..|]. unfold convert. case_eq (F.valid_lb xl); [|intros _ [H0 H1]; exfalso; lra]. case_eq (F.valid_ub xu); [|intros _ _ [H0 H1]; exfalso; lra]. intros Vxu Vxl. case_eq (F.valid_lb yl); [|intros _ _ [H0 H1]; exfalso; lra]. case_eq (F.valid_ub yu); [|intros _ _ _ [H0 H1]; exfalso; lra]. intros Vyu Vyl. intros (Hxl, Hxu) (Hyl, Hyu). simpl. elim (F.add_DN_correct prec xl yl); [|easy..]; intros H _; rewrite H; clear H. elim (F.add_UP_correct prec xu yu); [|easy..]; intros H _; rewrite H; clear H. apply le_contains. { apply (le_lower_trans _ (Xadd (F.toX xl) (F.toX yl))); [now apply F.add_DN_correct|]. revert Hxl Hyl. xreal_tac2; [now simpl|intro Hx]. xreal_tac2; [now simpl|intro Hy]. now apply Ropp_le_contravar, Rplus_le_compat. } apply (le_upper_trans _ (Xadd (F.toX xu) (F.toX yu))); [|now apply F.add_UP_correct]. revert Hxu Hyu. xreal_tac2; [now simpl|intro Hx]. xreal_tac2; [now simpl|intro Hy]. now apply Rplus_le_compat. Qed.
imports: Coq(Bool Reals Psatz) Flocq(Raux) Stdlib Xreal Basic Sig Interval