proposition: Lemma ex_derive_n_comp_scal (f : R -> R) (a : R) (n : nat) (x : R) : locally (a * x) (fun x => forall k, (k <= n)%nat -> ex_derive_n f k x) -> ex_derive_n (fun y => f (a * y)) n x.
proof: Proof. case: n f x => /= [ | n] f x Hf. by []. case: (Req_dec a 0) => Ha. rewrite Ha => {a Ha Hf}. apply ex_derive_ext with (fun _ => Derive_n (fun y : R => f (0 * y)) n 0). elim: n => /= [ | n IH] t. by rewrite ?Rmult_0_l. rewrite -?(Derive_ext _ _ _ IH). by rewrite ?Derive_const. by apply ex_derive_const. apply ex_derive_ext_loc with (fun x => a^n * Derive_n f n (a * x)). case: Hf => r Hf. have Hr0 : 0 < r / Rabs a. apply Rdiv_lt_0_compat. by apply r. by apply Rabs_pos_lt. exists (mkposreal _ Hr0) => /= y Hy. apply eq_sym, Derive_n_comp_scal. have : Rabs (a*y - a*x) < r. rewrite -Rmult_minus_distr_l Rabs_mult. replace (pos r) with (Rabs a * (r / Rabs a)) by (field ; by apply Rgt_not_eq, Rabs_pos_lt). apply Rmult_lt_compat_l. by apply Rabs_pos_lt. by apply Hy. move => {} Hy. apply Rabs_lt_between' in Hy ; case: Hy => Hy1 Hy2. apply Rlt_Rminus in Hy1. apply Rlt_Rminus in Hy2. exists (mkposreal _ (Rmin_pos _ _ Hy1 Hy2)) => /= z Hz k Hk. rewrite /ball /= /AbsRing_ball /= in Hz. apply Rabs_lt_between' in Hz ; case: Hz => Hz1 Hz2. rewrite /Rminus -Rmax_opp_Rmin in Hz1. rewrite Rplus_min_distr_l in Hz2. apply Rlt_le_trans with (2 := Rmin_r _ _) in Hz2. ring_simplify in Hz2. rewrite Rplus_max_distr_l in Hz1. apply Rle_lt_trans with (1 := Rmax_l _ _) in Hz1. ring_simplify in Hz1. apply Hf. apply Rabs_lt_between' ; by split. by intuition. apply ex_derive_scal. apply ex_derive_comp. apply (locally_singleton _ _) in Hf. by apply Hf with (k := S n). apply (ex_derive_scal id a x (ex_derive_id _)). Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Iter Hierarchy Continuity Equiv