proposition: Lemma cos_acos : forall x, -1 <= x <= 1 -> cos (acos x) = x.
proof: Proof. intros x xB. assert (H : x = -1 \/ -1 < x) by lra. destruct H as [He|Hl]. - rewrite He. change (IZR (-1)) with (-(IZR 1)). now rewrite acos_opp, acos_1, Rminus_0_r, cos_PI. - assert (H : x = 1 \/ x < 1) by lra. destruct H as [He1|Hl1]. { now rewrite He1, acos_1, cos_0. } rewrite acos_asin, cos_shift; try lra. rewrite sin_asin; lra. Qed.
imports: Lra Rbase PSeries_reg Rtrigo1 Rtrigo_facts Ranalysis_reg Rfunctions AltSeries Rseries SeqProp Ranalysis5 SeqSeries PartSum Lia