proposition: Lemma sqrt_mult : forall x y xpos ypos xypos, sqrt (x[*]y) xypos [=] sqrt x xpos[*]sqrt y ypos.
proof: Proof. intros. apply root_unique with 2. apply sqrt_nonneg. apply mult_resp_nonneg; apply sqrt_nonneg. auto. astepl (x[*]y). astepl (sqrt x xpos[^]2[*]sqrt y ypos[^]2). rational. Qed.
imports: CoRN.reals.OddPolyRootIR