proposition: Lemma acos_asin : forall x, -1 <= x <= 1 -> acos x = PI/2 - asin x.
proof: Proof. intros x. unfold acos, 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