Let $R = \Bbb C[[x]]$ the ring of formal power series and $A = R[\partial]$ the ring of differential operators with the relation $[\partial,x] = 1$. There is the following proposition in my book ("Eléments de la théorie des systèmes différentiels : D-modules cohérents et holonomes" by Maisonobe and Sabbah, at the beginning of chapter 1) :
Proposition : Let $P,A$ be differential operators. There is a unique couple of differential operators $(Q,R)$ so that $A = PQ + R$ and $R = \sum u_{k,l}x^k \partial^l + S$ where $u_{k,l}$ are invertible, $1 \leq k \leq v(P) -1, \deg(P) \leq l \leq \deg(A)$ and $\deg(S) < \deg(P)$.
Here, $\deg(P)$ is degree in $R[\partial]$ where $R$ has degree $0$ and $\partial$ has degree $1$. Also, $v(P)$ is the valuation of $a_d \in R$ where $P = a_d \partial^d + \text{lower order terms in }\partial$.
Instead of the proof it's written "Easy induction." but I can't see how to do it and I don't understand why these conditions are the correct one.
Question 1 : How to prove the proposition ?
Question 2 : What is a non trivial of a division in $A$, for example say $x^2\partial^3 + x$ divided by $x^2\partial + 1$ ?
Let me answer question 2 first, because it would hopefully illustrate how to approach question 1.
Answer to 2
To divide $x^2\partial^3+x$ by $x^2\partial+1$ (on the left), the obvious step is to compute $$ x^2\partial^3+x-(x^2\partial+1)\partial^2=x-\partial^2 $$ and now there is nothing more we can do, because $v(x^2\partial+1)=2\geq\max(v(x),v(-\partial^2))$ so we put this remainder term in $R$.
Answer to 1
In general you induct on degree of $A$. If the top ($\partial$-)degree term in $A$ has $v<v(P)$ we move this into the remainder and use induction hypothesis for the rest of $A$. Otherwise, we have $\dfrac{a_{\deg A}}{p_{\deg P}}\in\mathbb{C}[[x]]$ (where the lowercase letter is the coefficient of the corresponding uppercase differential operator) and then $A-P\dfrac{a_{\deg A}}{p_{\deg P}}\partial^{\deg A-\deg P}$ has a lower ($\partial$-)degree than $A$. This shows existence, and uniqueness is clear.