proposition: Lemma rotation_PI2 : forall x y:R, xr x y (PI / 2) = y /\ yr x y (PI / 2) = - x.
proof: Proof. intros x y; unfold xr, yr; split; rewrite cos_PI2; rewrite sin_PI2; ring. Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo1 R_sqrt