Are coefficients of a formal deformation bilinear? $\newcommand{\planck}\hbar$ I was given the following definition of formal deformation:

Let $A$ be an associative $R$-algebra with unit over a commutative ring. A formal deformation of $A$ is an associative algebra $(A[[\planck]], \star)$ where the product $\star$ is $R[[\planck]]$-bilinear and
  $$
 a \star b = ab + \sum_{n=1}^\infty \mu_n(a,b)\,\planck^n, \quad \forall a,b \in A[[\planck]]
$$
  where $ab$ denotes the canonical power series product of $a, b \in A[[\planck]]$.

A similar definition can be found in Formality and Star Products (Cattaneo) already specialized into the definition of star products.
My crux is: are the coefficients $\mu_n$ assumed to be $R[[\planck]]$-bilinear as well? I can't seem to derive this from the $R[[\planck]]$-bilinearity of $\star$ (while the opposite should be easy), and this seem necessary to prove associativity. In fact, the following was stated as a more or less 'trivial' fact:

Proposition. Given a formal deformation $(A[[\planck]], \star)$ of an associative unital $R$-algebra $A$ then
  $$
 \sum_{k=0}^n \mu_{n-k}(\mu_k(a,b), c)-\mu_{n-k}(a,\mu_k(b,c)) = 0, \quad \forall n \in \mathbb N, a,b,c \in A.
$$

Assuming $R[[\planck]]$-bilinearity of the $\mu_n$, this is indeed quite trivial:
Proof: The stated identity is derived from the associativity of $\star$, written ``degree-wise''.
$$
\begin{align}
 (a \star b) \star c &= a \star (b \star c)\\
 \left(\sum_{n=0}^\infty \mu_n(a,b)\,\planck^n \right) \star c &= a \star \left(\sum_{n=0}^\infty \mu_n(b,c)\,\planck^n\right)\\
 \sum_{n=0}^\infty \mu_n\left(\sum_{k=0}^\infty \mu_k(a,b)\,\planck^k,c \right)\,\planck^n &= \sum_{n=0}^\infty \mu_n\left(a, \sum_{k=0}^\infty \mu_k(b,c)\,\planck^k \right)\,\planck^n\\
 \sum_{n=0}^\infty \sum_{k=0}^\infty \mu_n(\mu_k(a,b),c)\,\planck^{k+n} &= \sum_{n=0}^\infty \sum_{k=0}^\infty \mu_n(a,\mu_k(b,c))\,\planck^{k+n}\\
 \sum_{k=0}^n \mu_{n-k}(\mu_k(a,b), c) &= \sum_{k=0}^n \mu_{n-k}(a,\mu_k(b,c)), \quad \forall n \in \mathbb N.
\end{align}
$$
Moreover, I found this old paper by Gerstenhaber in which (p. 62) he seems to assume the bilinearity of such coefficients (but it is not completely clear to me if he's talking about the same thing I'm talking about).
 A: After some investigation, it appears that the answer to my question is yes.
The main reason is informal: any reasonable example of deformation is built by  $R[[\hbar]]$-bilinear extension from bilinear forms on $A$, the undeformed algebra. This is especially true in deformation quantization, as the algebra $\mathcal{C}^\infty(M)$ is what we really care about.
Does this mean all deformations which arise from a similar bilinear extension? I believe the answer to be yes, as we can't show the $\mu_n$ to be bilinear simply by assuming the product is. The main obstruction is that coefficients of different degrees get mixed in a Cauchy-like product. Moreover, if we assume $\mu_n : A[[\hbar]] \times A[[\hbar]] \to A[[\hbar]]$, then also the coefficients of the coefficients (!!) get mixed. Eventually, your $n$th degree coefficient will involve three different indices mixing the $\mu_n$ and their own coefficients as well, making it unlikely that you can impose strong conditions on the single coefficients.
The point, indeed, is that we don't want the deformation to be just a product, but to have this particular form. In fact, it's obvious that any $R[[\hbar]]$-bilinear form arise from bilinear extension, but there are no guarantees on the expression of such an extension.
In the end, the updated definition of formal deformation would be the following (drawing from Gerstenhaber's paper linked in the question):

Let $A$ be an associative $R$-algebra. An $R[[\hbar]]$-bilinear form $A[[\hbar]] \times A[[\hbar]] \times A[[\hbar]]$ is said to be defined over $R$ whenever it is the $R[[\hbar]]$-bilinear extension of an $R$-bilinear form $A \times A \to A$.

The ''bilinear extension'' is defined functorially by completon (a kind of extension of scalars).

Let $A$ be an associative $R$-algebra with unit over a commutative ring. Let $\{\mu_n : A[[\hbar]] \times A[[\hbar]] \to A[[\hbar]]\}_{n \in \mathbb N}$ be a sequence of $R[[\hbar]]$-bilinear forms defined over $R$. A formal deformation of $A$ is then a product (associative but not necessarily unital) on $A[[\hbar]]$ having the following expression:
  $$
 a \star b = ab + \sum_{n=1}^\infty \mu_n(a,b)\,\hbar^n, \quad \forall a,b \in A[[\hbar]]
$$
  where $ab$ denotes the canonical power series product of $a, b \in A[[\hbar]]$.

