proposition: Lemma unary_bnd_correct : forall prec o xi x, contains (I.convert xi) (Xreal x) -> contains (I.convert (unary_bnd prec o xi)) (Xreal (unary_real o x)).
proof: Proof. intros prec o xi x. destruct o. apply I.neg_correct. apply I.abs_correct. apply J.inv_correct. apply I.sqr_correct. apply J.sqrt_correct. apply I.cos_correct. apply I.sin_correct. apply J.tan_correct. apply I.atan_correct. apply I.exp_correct. apply J.ln_correct. apply J.power_int_correct. apply I.nearbyint_correct. apply J.round_flt_correct. apply I.error_flt_correct. apply J.round_fix_correct. apply I.error_fix_correct. Qed.
imports: Coq(Reals List) Xreal Basic Interval