proposition: Lemma Derivative_I_n_cmul : forall (n : nat) (f f' : PartFunct IR) (c : IR), Derivative_I_n Hab n f f' -> Derivative_I_n Hab n (c{**}f) (c{**}f').
proof: Proof. intro n. induction n. intros. simpl. simpl in X. unfold Fscalmult. apply Feq_mult. apply Feq_reflexive. unfold included. simpl. auto. exact X. intros. simpl. destruct X. exists (IMult (IConst c) x). apply Derivative_I_wdr with ((Fconst c) {*} PartInt x). apply part_int_mult. apply part_int_const. apply Feq_reflexive. apply derivative_imp_inc' with f. exact d. apply Derivative_I_scal. exact d. apply Derivative_I_n_wdl with ((Fconst c) {*} PartInt x). apply part_int_mult. apply part_int_const. apply Feq_reflexive. apply derivative_imp_inc' with f. exact d. apply IHn. exact d0. 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