proposition: Lemma Derive_n_plus (f g : R -> R) (n : nat) (x : R) : locally x (fun y => forall k, (k <= n)%nat -> ex_derive_n f k y) -> locally x (fun y => forall k, (k <= n)%nat -> ex_derive_n g k y) -> Derive_n (fun x => f x + g x) n x = Derive_n f n x + Derive_n g n x.
proof: Proof. elim: n x => /= [ | n IH] x [rf Hf] [rg Hg]. by []. rewrite -Derive_plus. apply Derive_ext_loc. set r := (mkposreal _ (Rmin_stable_in_posreal rf rg)) ; exists r => y Hy. rewrite /ball /= /AbsRing_ball /= in Hy. apply Rabs_lt_between' in Hy. case: Hy ; move/Rlt_Rminus => Hy1 ; move/Rlt_Rminus => Hy2. set r0 := mkposreal _ (Rmin_pos _ _ Hy1 Hy2). apply IH ; exists r0 => z Hz k Hk. apply Hf. rewrite /ball /= /AbsRing_ball /= in Hz. apply Rabs_lt_between' in Hz. rewrite /Rminus -Rmax_opp_Rmin Rplus_max_distr_l (Rplus_min_distr_l y) in Hz. case: Hz ; move => Hz1 Hz2. apply Rle_lt_trans with (1 := Rmax_l _ _) in Hz1 ; ring_simplify in Hz1. apply Rlt_le_trans with (2 := Rmin_r _ _) in Hz2 ; ring_simplify (y + (x + Rmin rf rg + - y)) in Hz2. have Hz := (conj Hz1 Hz2) => {Hz1 Hz2}. apply Rabs_lt_between' in Hz. apply Rlt_le_trans with (1 := Hz) => /= ; by apply Rmin_l. by apply Nat.le_trans with (1 := Hk), Nat.le_succ_diag_r. apply Hg. rewrite /ball /= /AbsRing_ball /= in Hz. apply Rabs_lt_between' in Hz. rewrite /Rminus -Rmax_opp_Rmin Rplus_max_distr_l (Rplus_min_distr_l y) in Hz. case: Hz ; move => Hz1 Hz2. apply Rle_lt_trans with (1 := Rmax_l _ _) in Hz1 ; ring_simplify in Hz1. apply Rlt_le_trans with (2 := Rmin_r _ _) in Hz2 ; ring_simplify (y + (x + Rmin rf rg + - y)) in Hz2. have Hz := (conj Hz1 Hz2) => {Hz1 Hz2}. apply Rabs_lt_between' in Hz. apply Rlt_le_trans with (1 := Hz) => /= ; by apply Rmin_r. by apply Nat.le_trans with (1 := Hk), Nat.le_succ_diag_r. apply Hf with (k := (S n)). by apply ball_center. by apply Nat.le_refl. apply Hg with (k := S n). by apply ball_center. by apply Nat.le_refl. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Iter Hierarchy Continuity Equiv