proposition: Lemma sqrt_to_nonpos : forall x, x [<=] [0] -> forall x2pos, sqrt (x[^]2) x2pos [=] [--]x.
proof: Proof. intros. apply root_unique with 2. apply sqrt_nonneg. astepl ( [--]ZeroR). apply inv_resp_leEq. auto. auto. astepl (x[^]2). rational. Qed.
imports: CoRN.reals.OddPolyRootIR