proposition: Lemma sin_antisym : forall x:R, sin (- x) = - sin x.
proof: Proof. intro; unfold sin; replace (Rsqr (- x)) with (Rsqr x); [ idtac | apply Rsqr_neg ]. case (exist_sin (Rsqr x)); intros; ring. Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo_fun Lra Lia