An analogue of the Bass-Quillen conjecture with power or Laurent series

Here is an attempt at the power series question. One can easily reduce to the one variable case. So, I will attempt to prove that if $R$ is any Noetherian ring and $A=R[[x]]$ and $P$ a projective module, then $P\cong P/xP\otimes_R A =P'$, First, note that if $K$ is any finitely generated $A$ module, then it is complete with respect to the $x$-adic topology and so if $K=xK$, then $K=0$. Since $P'$ is $A$-projective, we can lift the surjective map $P'\to P/xP$ to a map $P'\to P$ which is an isomorphism mod $x$. Then the cokernel $K$ of $P'\to P$ has the property $K/xK=0$ and thus $K=0$. So, $P'\to P$ is surjective and so it splits. If $C$ is its kernel, then $C/xC=0$ and so $C=0$. Thus the map $P'\to P$ is an isomorphism.


I believe it should be possible to remove the "Noetherian" hypothesis in Mohan's answer, using the following slight generalization of the Nakayama-style fact:

Lemma: Let $f : R \to A$ be a ring map admitting a section $g : A \to R$ and such that the inclusion $A^{\times} \subseteq g^{-1}(R^{\times})$ is an equality. Let $K$ be a finitely presented $A$-module such that $K \otimes_{A,g} R = 0$. Then $K = 0$.

Proof: Let $$ A^{\oplus s} \stackrel{\varphi}{\to} A^{\oplus r} \to K \to 0 $$ be a presentation of $K$ as a $A$-module, and let $$ M \in \mathrm{Mat}_{r \times s}(A) $$ be the matrix corresponding to $\varphi$. Since $\varphi \otimes_{A,g} R$ is surjective, there exists $N \in \mathrm{Mat}_{s \times r}(R)$ such that $g(M) \cdot N = \operatorname{id}_{r}$, hence $g(M \cdot f(N)) = \operatorname{id}_{r}$, which means $M \cdot f(N)$ is invertible (since $A^{\times} = g^{-1}(R^{\times})$).

Remarks: I guess in this question we only consider finitely generated projective modules. To check that $K,C$ are finitely presented, we may use e.g. part (4) of [SP, 0519].