proposition: Lemma sin_acos : forall x, -1 <= x <= 1 -> sin (acos x) = sqrt (1 - x²).
proof: Proof. intros x Hxrange. pose proof (cos_acos x) ltac:(lra) as Hacos. remember (acos(x)) as α. rewrite <- Hacos. apply sin_cos. pose proof sin_ge_0 α. pose proof acos_bound x. lra. Qed.
imports: Lra Rbase PSeries_reg Rtrigo1 Rtrigo_facts Ranalysis_reg Rfunctions AltSeries Rseries SeqProp Ranalysis5 SeqSeries PartSum Lia