Yes, your proof is correct. Since it employs only the associative and commutativite axioms for multiplication it remains true in any commutative semigroup. The proof employs only the inference rules of first-order equational logic, namely that equality is an equivalence relation (reflexive, symmetric, transitive) and the rules of substitution: $p(x) = q(x) \rightarrow p(a) = q(a)$ and replacement: $a = b \rightarrow p(a) = p(b)$.
By a famous theorem of Birkhoff, for any algebraic structure that can be defined by axioms - like comutativity, associativity, etc - that are all universally quantified equations, said inference rules are complete, i.e. an equation is provable from the axioms using said inference rules iff it is true in every structure that satisfies the axioms. However, finding such a purely equational proof can be highly difficult. For example, consider the famous Jacobson theorem that rings satisfying the axiom $x^n = x \;$ are commutative $xy = yx$. it's notoriously difficult for $n>2$ to find equational proofs of this theorem.
Returning to the specific problem: generally scaling a polynomial $f(x)$ by a cancelable element $c$ does not change its solution set since $c f(d) = 0 \iff f(d) = 0$. In particular the solvability of $f(x) = 0$ is not altered - which is what you are concerned with in the definition of divisibility, i.e. the solvability of $ax = b$. E.g. consider the less trivial case of quadratic $f(x)$. Note that the formula $g(a,b,c)$ for the solutions of a quadratic $ax^2+bx+c$ remains unaltered by nonzero coefficient scalings $g(ad,bd,cd) = g(a,b,c)$. As for solvability, scaling the polynomial by $d$ multiplies the discriminant $b^2-4ac$ by $d^2$ so it does not affect the solvability criterion - that the discriminant be a perfect square. But we don't need to know these explicit formulas to deduce this. Rather, we can deduce it at a conceptually higher-level, simply from the cancelability of $c$, i.e the invertibility of scaling transformations $x\to cx$.