proposition: Lemma binary_bnd_correct : forall prec o xi yi x y, contains (I.convert xi) (Xreal x) -> contains (I.convert yi) (Xreal y) -> contains (I.convert (binary_bnd prec o xi yi)) (Xreal (binary_real o x y)).
proof: Proof. intros prec o xi yi x y. destruct o. apply I.add_correct. apply I.sub_correct. apply I.mul_correct. apply J.div_correct. Qed.
imports: Coq(Reals List) Xreal Basic Interval