proposition: Lemma asin_atan : forall x, -1 < x < 1 -> asin x = atan (x / sqrt (1 - x²)).
proof: Proof. intros x. unfold asin; repeat case Rle_dec; intros; lra. Qed.
imports: Lra Rbase PSeries_reg Rtrigo1 Rtrigo_facts Ranalysis_reg Rfunctions AltSeries Rseries SeqProp Ranalysis5 SeqSeries PartSum Lia