proposition: Lemma cos_sin_0_var : forall x:R, cos x <> 0 \/ sin x <> 0.
proof: Proof. intros x. destruct (Req_dec (cos x) 0). 2: now left. right. intros H'. apply (cos_sin_0 x). now split. Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo_fun Rtrigo_def Rtrigo_alt Cos_rel Cos_plus ZArith_base Zcomplements Lia Lra Ranalysis1 Rsqrt_def PSeries_reg