proposition: Lemma rad_deg : forall x:R, toRad (toDeg x) = x.
proof: Proof. intro; unfold toRad, toDeg; replace (x * plat * / PI * PI * / plat) with (x * (plat * / plat) * (PI * / PI)); [ idtac | ring ]. repeat rewrite Rinv_r. - ring. - apply PI_neq0. - unfold plat; discrR. Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo1 R_sqrt