proposition: Lemma derivable_pt_sqrt : forall x:R, 0 < x -> derivable_pt sqrt x.
proof: Proof. unfold derivable_pt; intros. exists (/ (2 * sqrt x)). apply derivable_pt_lim_sqrt; assumption. Qed.
imports: Rbase Rfunctions Ranalysis1 R_sqrt Lra