proposition: Lemma cos_fastP_correct : forall prec x, F.toX x = Xreal (toR x) -> (0 <= toR x)%R -> contains (I.convert (cos_fastP prec x)) (Xreal (cos (toR x))).
proof: Proof. intros prec x Hxr Hx0. unfold cos_fastP. case_eq (F'.le' x c1_2) ; intros H. { apply cos_fast0_correct. { easy. } rewrite Rabs_pos_eq with (1 := Hx0). apply F'.le'_correct in H. revert H. now rewrite c1_2_correct, Hxr. } generalize (S (Z2nat (F.StoZ (F.mag x)))) (F.incr_prec prec (Z2P (F.StoZ (F.mag x) + 6))). intros nb prec'. generalize (sin_cos_reduce_correct prec' nb x Hxr Hx0). destruct sin_cos_reduce as [ss ci]. apply proj1. Qed.
imports: Coq(Reals Psatz) Flocq(Zaux Raux Digits) Stdlib Xreal Basic Sig Interval Float