proposition: Theorem sin_fast_correct : forall prec x, contains (I.convert (sin_fast prec x)) (Xsin (F.toX x)).
proof: Proof. intros prec x. unfold sin_fast. rewrite F'.cmp_correct, F.zero_correct. case_eq (F.toX x). easy. intros r Hr. simpl. case Rcompare_spec ; intros H. rewrite <- (Xneg_involutive (Xreal _)). apply I.neg_correct. simpl. rewrite <- sin_neg. replace (Ropp r) with (toR (F.neg x)). apply sin_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. now rewrite F'.neg_correct, Hr. rewrite H, sin_0. simpl. rewrite F.zero_correct, F'.valid_lb_zero, F'.valid_ub_zero. split ; apply Rle_refl. replace r with (toR x). apply sin_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