proposition: Lemma sqrt_neg : forall x, (x <= 0)%R -> (sqrt x = 0)%R.
proof: Proof. intros x Npx. destruct (Req_dec x 0) as [Zx|Nzx]. - rewrite Zx. exact sqrt_0. - unfold sqrt. destruct Rcase_abs. + reflexivity. + exfalso. now apply Nzx, Rle_antisym; [|apply Rge_le]. Qed.
imports: Coq(Psatz Reals ZArith) Zaux