I am wondering what sort of results are available for the following sort of problem, or where to look in the literature for work dealing with such problems, especially in the degenerate elliptic context. It seems like there should be a general functional-analytic framework, but I'm not sure where to look.

Suppose that one has an order-$N$ (nonlinear) differential operator $P:C^\infty\to C^\infty$ which for any $k\geq N$ extends to a map $C^{k,\alpha}\to C^{k-N,\alpha}$ which is smooth as a map between Banach spaces. Suppose that $P$ has an inverse $Q:C^\infty\to C^\infty$. Suppose that there is $m\in\mathbb{N}$ such that, for any $k\geq 0$, $Q$ has a unique continuous extension to a map $C^{k,\alpha}\to C^{k+m,\alpha}$. Is $Q$ necessarily smooth as a map between these Banach spaces?