proposition: Lemma atan_fast_correct : forall prec x, contains (I.convert (atan_fast prec x)) (Xatan (F.toX x)).
proof: Proof. intros prec x. unfold atan_fast. rewrite F'.cmp_correct, F.zero_correct. case_eq (F.toX x) ; simpl. easy. intros r Hr. case Rcompare_spec ; intros H. rewrite <- (Ropp_involutive r). replace (Ropp r) with (toR (F.neg x)). rewrite atan_opp. apply (I.neg_correct _ (Xreal _)). apply atan_fastP_correct. unfold toR. now rewrite F'.neg_correct, Hr. unfold toR. rewrite F'.neg_correct, Hr. simpl. rewrite <- Ropp_0. now apply Ropp_le_contravar, Rlt_le. unfold toR. now rewrite F'.neg_correct, Hr. rewrite H, atan_0. simpl. rewrite F.zero_correct, F'.valid_lb_zero, F'.valid_ub_zero. split ; apply Rle_refl. replace r with (toR x). apply atan_fastP_correct. unfold toR. now rewrite Hr. unfold toR. rewrite Hr. now apply Rlt_le. unfold toR. now rewrite Hr. Qed.
imports: Coq(Reals Psatz) Flocq(Zaux Raux Digits) Stdlib Xreal Basic Sig Interval Float