proposition: Lemma cos_sin_0 : forall x:R, ~ (cos x = 0 /\ sin x = 0).
proof: Proof. intro; red in |- *; intro; elim H; intros; generalize (sin2_cos2 x); intro; rewrite H0 in H2; rewrite H1 in H2; repeat rewrite Rsqr_0 in H2; rewrite Rplus_0_r in H2; generalize Rlt_0_1; intro; rewrite <- H2 in H3; elim (Rlt_irrefl 0 H3). 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