proposition: Theorem tan_fast_correct : forall prec x, contains (I.convert (tan_fast prec x)) (Xtan (F.toX x)).
proof: Proof. intros prec x. unfold tan_fast. rewrite F'.cmp_correct, F.zero_correct. case_eq (F.toX x). easy. intros r Hr. simpl Xcmp. case Rcompare_spec ; intros H. rewrite <- (Xneg_involutive (Xtan _)). apply I.neg_correct. generalize (tan_fastP_correct prec (F.neg x)). unfold toR. rewrite F'.neg_correct, Hr. simpl. intros H'. assert (H1 : (0 <= -r)%R). rewrite <- Ropp_0. apply Ropp_le_contravar. now apply Rlt_le. specialize (H' eq_refl H1). revert H'. unfold Xtan'. simpl. rewrite cos_neg. case is_zero_spec. easy. intros _. now rewrite tan_neg. simpl. rewrite H, F.zero_correct. unfold Xtan'. simpl. case is_zero_spec. rewrite cos_0. intros H'. now elim R1_neq_R0. intros _. rewrite tan_0. rewrite F'.valid_lb_zero, F'.valid_ub_zero. split ; apply Rle_refl. replace r with (toR x). apply tan_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