proposition: Lemma tan_period : forall x, cos x <> 0 -> tan x = tan (x + PI).
proof: Proof. intros x H. unfold tan. rewrite sin_plus. rewrite cos_plus. rewrite cos_PI. rewrite sin_PI. do 2 rewrite Rmult_0_r. unfold Rminus. rewrite Ropp_0. do 2 rewrite Rplus_0_r. unfold Rdiv. rewrite Rinv_mult_distr. change (-1) with (-(1)). rewrite <- Ropp_inv_permute. field. apply H. discrR. apply H. discrR. Qed.
imports: Rbase Rtactic Lra Ranalysis Rfunctions Rtrigo_facts Rseries_def SeqProp Rextensionality Rpser_usual RIVT Rseries_facts Rsequence_cv_facts MyRIneq Tactics Rinterval Ranalysis_def Ranalysis_def_simpl Ranalysis_facts Ranalysis5