proposition: Lemma Derivative_I_nth : forall n, Derivative_I Hab' (F{^}S n) (nring (S n) {**} (F'{*}F{^}n)).
proof: Proof. unfold Fscalmult in |- *. intro; induction n as [| n Hrecn]. apply Derivative_I_wdl with F. FEQ. apply Derivative_I_wdr with F'. FEQ. assumption. apply Derivative_I_wdl with (F{*}F{^}S n). apply FNth_mult'; Included. apply Derivative_I_wdr with (F{*} ([-C-](nring (S n)) {*} (F'{*}F{^}n)) {+}F'{*}F{^}S n). apply eq_imp_Feq. Included. Included. intros; simpl in |- *. set (fx := F x (ProjIR1 (ProjIR1 Hx))) in *; simpl in (value of fx); fold fx in |- *. set (f'x := F' x (ProjIR1 (ProjIR2 (ProjIR2 (ProjIR1 Hx))))) in *; simpl in (value of f'x); fold f'x in |- *. set (fx' := F x (ProjIR2 (ProjIR2 (ProjIR2 (ProjIR1 Hx))))) in *; simpl in (value of fx'); fold fx' in |- *. set (f'x' := F' x (ProjIR1 (ProjIR2 Hx))) in *; simpl in (value of f'x'); fold f'x' in |- *. set (fx'' := F x (ProjIR2 (ProjIR2 Hx))) in *; simpl in (value of fx''); fold fx'' in |- *. set (f'x'' := F' x (ProjIR1 (ProjIR2 Hx'))) in *; simpl in (value of f'x''); fold f'x'' in |- *. set (fx''' := F x (ProjIR2 (ProjIR2 Hx'))) in *; simpl in (value of fx'''); fold fx''' in |- *. apply eq_transitive_unfolded with (fx[*]((nring n[+][1])[*](f'x[*]fx[^]n))[+]f'x[*](fx[^]n[*]fx)). astepl (fx[*]((nring n[+][1])[*](f'x[*]fx'[^]n))[+]f'x'[*](fx''[^]n[*]fx'')). repeat apply bin_op_wd_unfolded; try apply nexp_wd; unfold fx, f'x, fx', f'x', fx'' in |- *; rational. rstepl ((nring n[+][1][+][1])[*](f'x[*](fx[^]n[*]fx))). astepr ((nring n[+][1][+][1])[*](f'x''[*](fx'''[^]n[*]fx'''))). repeat apply bin_op_wd_unfolded; try apply nexp_wd; unfold fx, f'x, f'x'', fx''' in |- *; rational. Deriv. Qed.
imports: CoRN.ftc.Derivative