proposition: Lemma derive_pt_sqrt : forall (x:R) (pr:0 < x), derive_pt sqrt x (derivable_pt_sqrt _ pr) = / (2 * sqrt x).
proof: Proof. intros. apply derive_pt_eq_0. apply derivable_pt_lim_sqrt; assumption. Qed.
imports: Rbase Rfunctions Ranalysis1 R_sqrt Lra