proposition: Lemma D_ext: forall n f g, f == g -> D n f -> D n g.
proof: Proof. intro n ; induction n ; intros f g f_eq_g Dnf. constructor. inversion_clear Dnf. assert (g_deriv : derivable g) by (eapply derivable_ext ; eassumption). apply (D_S _ _ g_deriv), IHn with (derive _ pr). intro x ; unfold derive ; rewrite (pr_nu_var2 _ _ _ (pr x) (g_deriv x) f_eq_g) ; reflexivity. assumption. 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