proposition: Lemma Diffble_I_n_mult : forall (n : nat) (f g : PartFunct IR) (Pfdf : Diffble_I_n Hab n f) (Pgdf : Diffble_I_n Hab n g), Diffble_I_n Hab n (Fmult f g).
proof: Proof. intro n. induction n. intros. simpl. apply included_conj. simpl in Pfdf. exact Pfdf. simpl in Pgdf. exact Pgdf. intros. simpl. elim Pfdf. intros. inversion x. elim Pgdf. intros. inversion x1. assert (included (Compact (less_leEq _ _ _ Hab)) (Dom f)). apply derivative_imp_inc with (PartInt x0). exact X. assert (included (Compact (less_leEq _ _ _ Hab)) (Dom g)). apply derivative_imp_inc with (PartInt x2). exact X0. assert (Diffble_I Hab (f{*}g)). apply Diffble_I_mult. exact x. exact x1. exists X3. destruct X3. simpl. assert (Derivative_I Hab (f{*}g) ((f{*}PartInt x2){+}(PartInt x0{*}g))). apply Derivative_I_mult. exact X. exact X0. apply Diffble_I_n_wd with (f{*}PartInt x2{+}PartInt x0{*}g). apply Derivative_I_unique with (f{*}g). exact X3. exact d. apply Diffble_I_n_plus. apply IHn. apply le_imp_Diffble_I with (S n). omega. exact Pfdf. destruct x1. simpl in p0. apply Diffble_I_n_wd with (PartInt x1). apply Derivative_I_unique with g. exact d0. exact X0. exact p0. apply IHn. destruct x. simpl in p. apply Diffble_I_n_wd with (PartInt x). apply Derivative_I_unique with f. exact d0. exact X. exact p. apply le_imp_Diffble_I with (S n). omega. exact Pgdf. 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