proposition: Lemma continuity_pt_sqrt : forall x:R, 0 <= x -> continuity_pt sqrt x.
proof: Proof. intros; case (Rtotal_order 0 x); intro. { apply (sqrt_continuity_pt x H0). } elim H0; intro. 2:exfalso;lra. unfold continuity_pt; unfold continue_in; unfold limit1_in; unfold limit_in; simpl; unfold Rdist; intros. exists (Rsqr eps); intros. split. { change (0 < Rsqr eps); apply Rsqr_pos_lt;lra. } intros; elim H3; intros. rewrite <- H1; rewrite sqrt_0; unfold Rminus; rewrite Ropp_0; rewrite Rplus_0_r; rewrite <- H1 in H5; unfold Rminus in H5; rewrite Ropp_0 in H5; rewrite Rplus_0_r in H5. destruct (Rcase_abs x0) as [Hlt|Hgt] eqn:Heqs. { unfold sqrt. rewrite Heqs. rewrite Rabs_R0; apply H2. } rewrite Rabs_right. 2: apply Rle_ge; apply sqrt_positivity; apply Rge_le; exact Hgt. apply Rsqr_incrst_0. - rewrite Rsqr_sqrt. + rewrite (Rabs_right x0 Hgt) in H5; apply H5. + apply Rge_le; exact Hgt. - apply sqrt_positivity; apply Rge_le; exact Hgt. - left; exact H2. Qed.
imports: Rbase Rfunctions Ranalysis1 R_sqrt Lra