proposition: Lemma tan_asin : forall x, -1 <= x <= 1 -> tan (asin x) = x / sqrt (1 - x²).
proof: Proof. intros x Hxrange. pose proof (sin_asin x) Hxrange as Hasin. remember (asin(x)) as α. rewrite <- Hasin. apply tan_sin. pose proof cos_ge_0 α. pose proof asin_bound x. lra. Qed.
imports: Lra Rbase PSeries_reg Rtrigo1 Rtrigo_facts Ranalysis_reg Rfunctions AltSeries Rseries SeqProp Ranalysis5 SeqSeries PartSum Lia