proposition: Lemma sin_PI : sin PI = 0.
proof: Proof. assert (H := sin2_cos2 PI). rewrite cos_PI in H. change (-1) with (-(1)) in H. rewrite <- Rsqr_neg in H. rewrite Rsqr_1 in H. cut (Rsqr (sin PI) = 0). - intro; apply (Rsqr_eq_0 _ H0). - apply Rplus_eq_reg_l with 1. rewrite Rplus_0_r; rewrite Rplus_comm; exact H. 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