proposition: Lemma Diffble_I_n_const : forall (n : nat) (c : IR), Diffble_I_n Hab n (Fconst c).
proof: Proof. intro n. induction n. intro c. simpl. unfold included. auto. intro c. simpl. assert (Diffble_I Hab [-C-] c). apply Diffble_I_const. exists X. destruct X. simpl. assert (Derivative_I Hab [-C-]c [-C-]Zero). apply Derivative_I_const. apply Diffble_I_n_wd with ([-C-]Zero). apply Derivative_I_unique with ([-C-]c). exact X. exact d. apply IHn. 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