proposition: Lemma Derivative_I_n_add : forall (n : nat) (f g f' g' : PartFunct IR) (Pfderiv : Derivative_I_n Hab n f f') (Pgderiv : Derivative_I_n Hab n g g'), Derivative_I_n Hab n (f{+}g) (f'{+}g').
proof: Proof. intro n. induction n. intros. apply Feq_plus. exact Pfderiv. exact Pgderiv. intros. simpl. elim Pfderiv. intros. elim Pgderiv. intros. exists (IPlus x x0). apply Derivative_I_wdr with (PartInt x{+}PartInt x0). apply part_int_plus. apply Feq_reflexive. apply derivative_imp_inc' with f. exact p. apply Feq_reflexive. apply derivative_imp_inc' with g. exact p0. apply Derivative_I_plus. exact p. exact p0. apply Derivative_I_n_wdl with (PartInt x{+}PartInt x0). apply part_int_plus. apply Feq_reflexive. apply derivative_imp_inc' with f. exact p. apply Feq_reflexive. apply derivative_imp_inc' with g. exact p0. apply IHn. exact q. exact q0. Qed.
imports: ssreflect CSetoids CSetoidFun CFields CPolynomials Program Omega Equivalence Morphisms Wf Morphisms CRings CRing_Homomorphisms Rational Setoid CPoly_NthCoeff CPoly_Degree CReals Intervals CauchySeq IntervalFunct MoreIntervals MoreFunctions Composition seq bigopsClass Structures