proposition: Lemma asin_1 : asin 1 = PI / 2.
proof: Proof. unfold asin; repeat case Rle_dec; lra. Qed.
imports: Lra Rbase PSeries_reg Rtrigo1 Rtrigo_facts Ranalysis_reg Rfunctions AltSeries Rseries SeqProp Ranalysis5 SeqSeries PartSum Lia