proposition: Lemma derivable_pt_lim_Rsqr : forall x:R, derivable_pt_lim Rsqr x (2 * x).
proof: Proof. intro; unfold derivable_pt_lim. unfold Rsqr; intros eps Heps; exists (mkposreal eps Heps); intros h H1 H2; replace (((x + h) * (x + h) - x * x) / h - 2 * x) with h. - assumption. - replace ((x + h) * (x + h) - x * x) with (2 * x * h + h * h); [ idtac | ring ]. unfold Rdiv; rewrite Rmult_plus_distr_r. repeat rewrite Rmult_assoc. repeat rewrite Rinv_r; [ idtac | assumption ]. ring. Qed.
imports: Rbase Rfunctions Rlimit Rderiv