Let K be a henselian valued field of characteristic 0. Then K admits a
definable partition on each piece of which the leading term of a polynomial in
one variable can be computed as a definable function of the leading term of a
linear map. Two applications are given: first, a constructive quantifier
elimination relative to the leading terms, suggesting a relative decision
procedure; second, a presentation of every definable subset of K as the
pullback of a definable set in the leading terms subjected to a linear
translation.