proposition: Lemma Diffble_I_n_minus : 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 (f{-}g).
proof: Proof. intros. assert ({f0' : CSetoid_fun (subset (Compact (less_leEq _ _ _ Hab))) IR | Derivative_I_n Hab n f (PartInt f0')}). apply Diffble_I_n_imp_deriv_n. exact Pfdf. assert ({g' : CSetoid_fun (subset (Compact (less_leEq _ _ _ Hab))) IR | Derivative_I_n Hab n g (PartInt g')}). apply Diffble_I_n_imp_deriv_n. exact Pgdf. inversion_clear X. inversion_clear X0. apply deriv_n_imp_Diffble_I_n with (PartInt x{-}PartInt x0). apply Derivative_I_n_minus. exact X1. exact X. 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