proposition: Lemma acos_cos : forall x, 0 <= x <= PI -> acos (cos x) = x.
proof: Proof. intros x HB. apply cos_inj; try lra. { apply acos_bound. } apply cos_acos. apply COS_bound. Qed.
imports: Lra Rbase PSeries_reg Rtrigo1 Rtrigo_facts Ranalysis_reg Rfunctions AltSeries Rseries SeqProp Ranalysis5 SeqSeries PartSum Lia