proposition: Lemma asin_opp : forall x, asin (- x) = - asin x.
proof: Proof. intros x. unfold asin; repeat case Rle_dec; intros; try lra. rewrite <- Rsqr_neg. rewrite Rdiv_opp_l. rewrite atan_opp. reflexivity. Qed.
imports: Lra Rbase PSeries_reg Rtrigo1 Rtrigo_facts Ranalysis_reg Rfunctions AltSeries Rseries SeqProp Ranalysis5 SeqSeries PartSum Lia