proposition: Lemma continuous_sqrt (x : R) : continuous sqrt x.
proof: Proof. destruct (Rle_or_lt 0 x) as [Hx|Hx]. apply continuity_pt_filterlim. by apply: continuity_pt_sqrt. assert (Hs: forall t, t < 0 -> sqrt t = 0). intros t Ht. unfold sqrt. case Rcase_abs. easy. intros Ht'. now elim Rge_not_lt with (1 := Ht'). intros P H. rewrite Hs // in H. unfold filtermap. eapply locally_open. apply open_lt. 2: exact Hx. move => /= t Ht. rewrite Hs //. now apply locally_singleton. Qed.
imports: Coq(Reals Psatz) Coquelicot(Coquelicot) mathcomp.ssreflect(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype bigop) Stdlib MathComp