proposition: Lemma sqrt_mult_wd : forall x y z xpos ypos zpos, z [=] x[*]y -> sqrt z zpos [=] sqrt x xpos[*]sqrt y ypos.
proof: Proof. intros. cut ([0] [<=] x[*]y). intro. Step_final (sqrt (x[*]y) H0). apply mult_resp_nonneg; auto. Qed.
imports: CoRN.reals.OddPolyRootIR