add compatibility lemmas for Stdlib Rcos and Rsin

[t6s]

Motivation for this change

Context:
https://rocq-prover.zulipchat.com/#narrow/channel/237666-math-comp-analysis/topic/relating.20trigo.2Ecos.20to.20Rtrigo_def.2Ecos.2C.20etc.2E

This PR adds compatibility lemmas for a few trigonometry functions defined in Stdlib Reals,
namely Rcos and Rsin. A lemma for π is also added.

Checklist

• added corresponding entries in CHANGELOG_UNRELEASED.md

• added corresponding documentation in the headers

Reference: How to document

Merge policy

As a rule of thumb:

• PRs with several commits that make sense individually and that
  all compile are preferentially merged into master.
• PRs with disorganized commits are very likely to be squash-rebased.

Reminder to reviewers

• Read this Checklist
• Put a milestone if possible
• Check labels

[t6s]

The proof turned out to be not as simple as for the exp case, due to a subtle difference in the defining series for Rcos and cos:
the former is
1 - (x^2/2!) + (x^4/4!) ...
while the latter is
1 + 0 - (x^2/2!) + 0 + (x^4/4!) + 0 ...

That said, the proof script for RcosE seems a bit too long, and there could be a better proof strategy.

[proux01]

The proof turned out to be not as simple as for the exp case, due to a subtle difference in the defining series for Rcos and cos: the former is 1 - (x^2/2!) + (x^4/4!) ... while the latter is 1 + 0 - (x^2/2!) + 0 + (x^4/4!) + 0 ...

Could cos_coeff' and cos_coeff'E help here?

[t6s]

The proof turned out to be not as simple as for the exp case, due to a subtle difference in the defining series for Rcos and cos: the former is 1 - (x^2/2!) + (x^4/4!) ... while the latter is 1 + 0 - (x^2/2!) + 0 + (x^4/4!) + 0 ...

Could cos_coeff' and cos_coeff'E help here?

That helps so much!!

[affeldt-aist]

By the way, this is not a useful comment anymore since the need has disappeared, but big_nat_dvdn should have gone to mathcomp_compat.v rather than unstable.

[proux01]

Let's merge after CI confirmation.