proposition: Lemma derive_pt_comp : forall f g x prf prg pr, derive_pt (comp g f)%F x pr = derive_pt f x prf * derive_pt g (f x) prg.
proof: Proof. intros f g x prf prg pr ; erewrite pr_nu_var with (pr2 := derivable_pt_comp _ _ x prf prg) ; [ rewrite Rmult_comm ; apply derive_pt_comp | reflexivity ]. Qed.
imports: Rbase Rpower Ranalysis Lra Rfunctions Rfunction_def Rextensionality MyRIneq MyR_dist Rtopology Rinterval Ranalysis_def Ranalysis_def_simpl Ranalysis_continuity Ranalysis_derivability Ranalysis_monotonicity