fact: Definition asin x := if Rle_dec x (-1) then - (PI / 2) else if Rle_dec 1 x then PI / 2 else atan (x / sqrt (1 - x²)).
imports: Lra Rbase PSeries_reg Rtrigo1 Rtrigo_facts Ranalysis_reg Rfunctions AltSeries Rseries SeqProp Ranalysis5 SeqSeries PartSum Lia