proposition: Lemma sin2PI_period : forall x k, sin x = sin (x + 2 * IZR ( k ) * PI).
proof: Proof. intros; symmetry. destruct k. f_equal. ring. unfold IZR. rewrite <-2INR_IPR. apply sin_period. unfold IZR. replace (x + IPR 2 * - IPR p * PI) with (x - (0 + IPR 2 * IPR p * PI)) by ring. rewrite <-2INR_IPR. rewrite sin_minus, cos_period, sin_period, cos_0, sin_0. ring. Qed.
imports: Rbase Rtactic Lra Ranalysis Ranalysis5 Rtrigo AltSeries Rfunctions Rinterval Ranalysis_def Ranalysis_def_simpl Ranalysis_facts Rextensionality Rpser_usual Rsequence_cv_facts MyRIneq Tactics