proposition: Lemma C_infty_comp : forall f g, C_infty f -> C_infty g -> C_infty (comp f g).
proof: Proof. intros f g Cf Cg n ; apply C_comp ; trivial. Qed.
imports: Rbase Ranalysis Lia Lra Rfunctions Rfunction_facts Rextensionality Rinterval Ranalysis_def Ranalysis_def_simpl Ranalysis_facts Ranalysis_continuity Ranalysis_derivability Ranalysis_monotonicity Rfunction_classes_def MyR_dist Reals.Tactics