diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index c676bc2941..253eb2e83d 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -52,6 +52,9 @@
   + global instance `is_derive_exp`
   + lemma `derive1_shift`
 
+- in `Rstruct_topology.v`:
+  + lemmas `RcosE`, `Rtrigo_PIE`, `RsinE`
+
 ### Changed
 
 - in `derive.v`:
@@ -69,6 +72,9 @@
 - moved from `realfun.v` to `derive.v`: 
   + lemmas `is_deriveV`, `is_derive1_comp`
 
+- in `Rstruct_topology.v`:
+  + lemma `RealsE` to include `RcosE`, `Rtrigo_PIE`, `RsinE`
+
 ### Renamed
 
 - in `esum.v`:
diff --git a/analysis_stdlib/Rstruct_topology.v b/analysis_stdlib/Rstruct_topology.v
index 2fa87fe480..ce7fe4028d 100644
--- a/analysis_stdlib/Rstruct_topology.v
+++ b/analysis_stdlib/Rstruct_topology.v
@@ -9,13 +9,16 @@ From Stdlib Require Import Epsilon FunctionalExtensionality Ranalysis1 Rsqrt_def
 From Stdlib Require Import Rtrigo1 Reals.
 From HB Require Import structures.
 From mathcomp Require Import boot order ssralg ssrnum archimedean.
+From mathcomp Require Import interval arithmetic_tactic.
 From mathcomp Require Import boolp classical_sets reals interval_inference.
 From mathcomp Require Export Rstruct.
 From mathcomp Require Import topology.
-(* The following line is for RexpE. *)
+(* The following line is for RexpE and RcosE. *)
 From mathcomp Require normedtype sequences.
 (* The following line is for RlnE. *)
 From mathcomp Require exp.
+(* The following line is for RcosE, PIE and RsinE. *)
+From mathcomp Require trigonometry_functions.
 
 Unset SsrOldRewriteGoalsOrder.  (* remove the line when requiring MathComp >= 2.6 *)
 Set Implicit Arguments.
@@ -120,5 +123,71 @@ case: (Rlt_dec 0 x) => [/= ? | /RltP/[!xgt0]//].
 by case: ln_exists => y ->; rewrite RexpE exp.expRK.
 Qed.
 
+Module RtrigoE.
+Import normedtype sequences trigonometry_functions.
+Local Open Scope classical_set_scope.
+
+Lemma RcosE (x : R) : Rtrigo_def.cos x = cos x.
+Proof.
+rewrite /Rtrigo_def.cos.
+case: exist_cos => y.
+rewrite /cos_in /cos_n /infinite_sum/=.
+set G : nat -> R^o := (G in sum_f_R0 G).
+move=> cos_ub.
+have /(@cvg_lim R^o) <- // : series G x @[x --> \oo] --> y.
+  rewrite -cvg_shiftS/=; apply/cvgrPdist_lt => /= e /RltP /cos_ub[N Ncos_ub].
+  near=> n.
+  have nN : (n >= N)%coq_nat by apply/ssrnat.leP; near: n; exact: nbhs_infty_ge.
+  move: Ncos_ub => /(_ _ nN) /[!RdistE] /RltP /=.
+  by rewrite /G distrC sum_f_R0E.
+apply: (@cvg_lim R^o) => //.
+suff -> : G = cos_coeff' x by exact: cvg_cos_coeff'.
+apply/funext=> n; rewrite /G cos_coeff'E cos_coeffE.
+rewrite odd_double/= mul1r plusE addn0 addnn Rsqr_def !RealsE.
+by rewrite -expr2 -exprM mul2n doubleK.
+Unshelve. all: by end_near. Qed.
+
+Section PIE.
+
+Let pihalf_spec (x : R) := 0 <= x <= 2 /\ cos x = 0.
+
+Let pihalf_unique (x y : R) : pihalf_spec x -> pihalf_spec y -> x = y.
+Proof.
+case=> /andP[] x0 x2 cosx0 [] /andP[] y0 y2 cosy0.
+apply: cos_inj.
+- rewrite in_itv/=; apply/andP; split => //.
+  by rewrite (le_trans x2)// pi_ge2.
+- rewrite in_itv/=; apply/andP; split => //.
+  by rewrite (le_trans y2)// pi_ge2.
+by rewrite cosx0 cosy0.
+Qed.
+
+Let PI2E : PI2 = pi / 2.
+Proof.
+rewrite /PI2; case: PI_2_aux => x /= [] [] /RleP x78 /RleP x74.
+move/Ropp_eq_compat; rewrite Ropp_involutive Ropp_0 RealsE => cosx0.
+rewrite pihalfE.
+have x_pihalf : pihalf_spec x.
+  split; [|by rewrite -RcosE].
+  rewrite (le_trans _ x78)/= ?RealsE/=; [lra|].
+  by rewrite (le_trans x74)// ?RealsE/=; lra.
+apply/esym/get_unique => //= y y_pihalf.
+exact: pihalf_unique.
+Qed.
+
+Lemma PIE : PI = pi.
+Proof. by rewrite /PI PI2E !RealsE/= mulrCA divff// mulr1. Qed.
+
+End PIE.
+
+Lemma RsinE (x : R) : Rtrigo_def.sin x = sin x.
+Proof. by rewrite sin_cos RcosE PIE !RealsE/= addrC cosDpihalf opprK. Qed.
+
+End RtrigoE.
+
+Definition RcosE := RtrigoE.RcosE.
+Definition Rtrigo_PIE := RtrigoE.PIE.
+Definition RsinE := RtrigoE.RsinE.
+
 (* extend RealsE from Rstruct.v *)
-Definition RealsE := (RealsE, RexpE, RlnE).
+Definition RealsE := (RealsE, RexpE, RlnE, RcosE, Rtrigo_PIE, RsinE).
diff --git a/classical/unstable.v b/classical/unstable.v
index 3d634c27c1..cfa0e8083a 100644
--- a/classical/unstable.v
+++ b/classical/unstable.v
@@ -9,7 +9,7 @@ From mathcomp Require Import vector archimedean interval matrix.
 (* This files contains lemmas that should eventually be backported            *)
 (* to mathcomp. These lemmas may change before being backported to mathcomp,  *)
 (* don't use anything in this file outside of Analysis. For this same reason, *)
-(* nothing in this file should be mentionned in the changelog.                *)
+(* nothing in this file should be mentioned in the changelog.                 *)
 (* Once a result is backported to mathcomp, please move it to mathcomp_extra.v*)
 (* and mention it in the changelog.                                           *)
 (*                                                                            *)