proposition: Lemma continuity_exp f n: continuity f -> continuity (fun x => (f x)^+ n)%R.
proof: Proof. move=> Hf; elim: n=> [|n IHn]; first exact: continuity_const. set g:= fun _ => _. have Hg: (fun x=> f x * f x ^+ n)%R =1 g. by move=> x; rewrite /g exprS. by apply: (continuity_eq Hg); exact: continuity_mult. Qed.
imports: Rdefinitions Raxioms RIneq Rbasic_fun Zwf Epsilon FunctionalExtensionality Ranalysis1 Rsqrt_def Rtrigo1 Reals mathcomp(all_ssreflect ssralg poly mxpoly ssrnum) HB(structures)