proposition: Lemma L_diffble_all_n : forall (f : C_inf_ab c d Hcd) (n : nat), Diffble_I_n Hab n (L_func f).
proof: Proof. intros. apply L_diffble. 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