proposition: Theorem cos_fast_correct : forall prec x, contains (I.convert (cos_fast prec x)) (Xcos (F.toX x)).
proof: Proof. intros prec x. unfold cos_fast. rewrite F'.cmp_correct, F.zero_correct. case_eq (F.toX x). easy. intros r Hr. simpl. case Rcompare_spec ; intros H. replace r with (- toR (F.neg x))%R. rewrite cos_neg. apply cos_fastP_correct. unfold toR. now rewrite F'.neg_correct, Hr. unfold toR. rewrite F'.neg_correct, Hr. rewrite <- Ropp_0. apply Ropp_le_contravar. now apply Rlt_le. unfold toR. rewrite F'.neg_correct, Hr. apply Ropp_involutive. rewrite H, cos_0. unfold c1. simpl. rewrite F'.valid_lb_real, F'.valid_ub_real by now rewrite F.real_correct, F.fromZ_correct. rewrite F.fromZ_correct by easy. split ; apply Rle_refl. replace r with (toR x). apply cos_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