[proofplan]
The theorem is a high-frequency elliptic parametrix statement, so the residual class must be ordinary smoothing rather than $h^\infty$ smoothing. We first invert the symbol on the region where the ellipticity estimate is available and record that the low-frequency error is merely in $S^{-\infty}_{1,0}$. We then construct a left symbolic inverse and a right symbolic inverse in the quotient of the symbol algebra by $S^{-\infty}_{1,0}$, use semiclassical asymptotic summation to realize the formal inverses, and finally compare the two inverses to obtain one symbol giving both operator identities.
[/proofplan]
[step:Invert the symbol on the high-frequency elliptic region]
Choose a function $\rho\in C^\infty(\mathbb{R}^n;[0,1])$ such that $\rho(\xi)=0$ for $|\xi|\leq R$ and $\rho(\xi)=1$ for $|\xi|\geq 2R$. Define
\begin{align*}
b_0:T^*\mathbb{R}^n\times(0,h_0]&\to\mathbb{C}
\end{align*}
by
\begin{align*}
b_0(x,\xi;h)=\rho(\xi)a(x,\xi;h)^{-1}.
\end{align*}
This is well-defined because $\rho$ is supported in the region $|\xi|\geq R$, where the ellipticity estimate implies $a(x,\xi;h)\neq0$.
We use the standard reciprocal-symbol lemma: if $a\in S^m_{1,0}$ and $|a|\geq c\langle\xi\rangle^m$ on an open conic-at-infinity region, then $a^{-1}\in S^{-m}_{1,0}$ on that region. The hypotheses are satisfied on $\{|\xi|>R\}$ by the stated ellipticity bound and by $a\in S^m_{1,0}$. Multiplication by the fixed cutoff $\rho$ preserves symbol order, so $b_0\in S^{-m}_{1,0}(T^*\mathbb{R}^n)$. Moreover
\begin{align*}
b_0a-1=\rho-1.
\end{align*}
The symbol $\rho-1$ is supported in $\{|\xi|\leq2R\}$, and every $\xi$-derivative of it is also compactly supported. Hence $\rho-1\in S^{-N}_{1,0}(T^*\mathbb{R}^n)$ for every $N\in\mathbb{N}$, uniformly in $h$, so $\rho-1\in S^{-\infty}_{1,0}$. This is exactly an ordinary smoothing-order error; no factor $h^N$ is obtained or needed.
[guided]
The ellipticity hypothesis only says that $a$ is invertible for large $|\xi|$. Therefore we cannot define the first inverse as $a^{-1}$ on all of $T^*\mathbb{R}^n$. We avoid the possible zeros at bounded covariables by choosing a cutoff $\rho\in C^\infty(\mathbb{R}^n;[0,1])$ with $\rho(\xi)=0$ for $|\xi|\leq R$ and $\rho(\xi)=1$ for $|\xi|\geq2R$, and we define
\begin{align*}
b_0:T^*\mathbb{R}^n\times(0,h_0]&\to\mathbb{C}
\end{align*}
by
\begin{align*}
b_0(x,\xi;h)=\rho(\xi)a(x,\xi;h)^{-1}.
\end{align*}
This definition is legitimate because $\rho(\xi)$ can be nonzero only where $|\xi|\geq R$, and the stated lower bound gives $|a(x,\xi;h)|\geq c\langle\xi\rangle^m>0$ there.
We now check the symbol order. The standard reciprocal-symbol lemma says that a symbol $a\in S^m_{1,0}$ satisfying $|a|\geq c\langle\xi\rangle^m$ on a region has reciprocal in $S^{-m}_{1,0}$ on that region. Its proof differentiates $a^{-1}$ repeatedly: each derivative is a finite sum of products containing powers of $a^{-1}$ and derivatives of $a$, and the lower bound on $a$ balances the symbol estimates for the derivatives of $a$. Since our hypotheses are precisely $a\in S^m_{1,0}$ and the displayed lower bound on $\{|\xi|\geq R\}$, the lemma applies on that region. Multiplying by the fixed smooth cutoff $\rho$ does not increase symbol order, hence $b_0\in S^{-m}_{1,0}$.
Finally we compute the first product at the symbolic level:
\begin{align*}
b_0a-1=\rho-1.
\end{align*}
The function $\rho-1$ is supported where $|\xi|\leq2R$. A compactly supported function of $\xi$ satisfies every negative-order symbol estimate, because $\langle\xi\rangle^N$ is bounded on its support for each $N\in\mathbb{N}$. Thus $\rho-1\in S^{-N}_{1,0}$ for every $N$, uniformly in $h$, and therefore $\rho-1\in S^{-\infty}_{1,0}$. This is the point at which the theorem deliberately uses ordinary smoothing remainders: compact support in $\xi$ gives infinite symbolic order, but it does not produce rapid powers of $h$.
[/guided]
[/step]
[step:Construct a left inverse in the quotient by smoothing symbols]
Let $\#$ denote the left semiclassical symbol product, characterized by the standard composition theorem
\begin{align*}
\operatorname{Op}_h(p)\operatorname{Op}_h(q)=\operatorname{Op}_h(p\# q)
\end{align*}
for $p\in S^r_{1,0}$ and $q\in S^s_{1,0}$, with asymptotic expansion
\begin{align*}
p\#q\sim\sum_{\alpha\in\mathbb{N}_0^n}\frac{h^{|\alpha|}}{i^{|\alpha|}\alpha!}\partial_\xi^\alpha p\,\partial_x^\alpha q.
\end{align*}
The theorem applies because $b_0\in S^{-m}_{1,0}$ and $a\in S^m_{1,0}$.
We recursively construct symbols $b_j\in S^{-m-j}_{1,0}$ for $j\in\mathbb{N}_0$. Suppose $b_0,\dots,b_{j-1}$ have been chosen so that, for
\begin{align*}
c_{j-1}=\sum_{k=0}^{j-1}h^k b_k,
\end{align*}
one has
\begin{align*}
c_{j-1}\#a-1\in h^jS^{-j}_{1,0}+S^{-\infty}_{1,0}.
\end{align*}
Choose $e_j\in S^{-j}_{1,0}$ such that
\begin{align*}
c_{j-1}\#a-1-h^je_j\in h^{j+1}S^{-j-1}_{1,0}+S^{-\infty}_{1,0}.
\end{align*}
Define
\begin{align*}
b_j:T^*\mathbb{R}^n\times(0,h_0]&\to\mathbb{C}
\end{align*}
by
\begin{align*}
b_j(x,\xi;h)=-\rho(\xi)e_j(x,\xi;h)a(x,\xi;h)^{-1}.
\end{align*}
The reciprocal-symbol lemma gives $b_j\in S^{-m-j}_{1,0}$. Since $\rho a^{-1}a=\rho$ and $1-\rho\in S^{-\infty}_{1,0}$, the leading contribution of $h^jb_j\#a$ is $-h^je_j$ modulo $h^{j+1}S^{-j-1}_{1,0}+S^{-\infty}_{1,0}$. Hence
\begin{align*}
(c_{j-1}+h^jb_j)\#a-1\in h^{j+1}S^{-j-1}_{1,0}+S^{-\infty}_{1,0}.
\end{align*}
Induction produces a formal left inverse $\sum_{j=0}^\infty h^jb_j$ modulo $S^{-\infty}_{1,0}$.
[/step]
[step:Realize the left formal inverse by asymptotic summation]
By the standard asymptotic summation theorem for semiclassical symbols, applied to the sequence $b_j\in S^{-m-j}_{1,0}$, there exists $b_L\in S^{-m}_{1,0}$ such that
\begin{align*}
b_L-\sum_{j=0}^{N-1}h^jb_j\in h^NS^{-m-N}_{1,0}
\end{align*}
for every $N\in\mathbb{N}$. The hypotheses of the theorem are satisfied because the orders $-m-j$ tend to $-\infty$. Combining this asymptotic realization with the recursive cancellation gives
\begin{align*}
b_L\#a-1\in S^{-\infty}_{1,0}.
\end{align*}
Quantizing the identity and using the standard fact that symbols in $S^{-\infty}_{1,0}$ quantize to ordinary uniformly smoothing semiclassical operators gives
\begin{align*}
\operatorname{Op}_h(b_L)A_h=I+R_h
\end{align*}
for some $R_h\in\Psi_h^{-\infty}(\mathbb{R}^n)$.
[/step]
[step:Construct a right inverse and compare it with the left inverse]
Applying the same construction to the product $a\#b$ gives a symbol $b_R\in S^{-m}_{1,0}$ such that
\begin{align*}
a\#b_R-1\in S^{-\infty}_{1,0}.
\end{align*}
Therefore
\begin{align*}
A_h\operatorname{Op}_h(b_R)=I+S_{R,h}
\end{align*}
for some $S_{R,h}\in\Psi_h^{-\infty}(\mathbb{R}^n)$.
We now compare $b_L$ and $b_R$ in the quotient algebra $S^*_{1,0}/S^{-\infty}_{1,0}$. The semiclassical product is associative modulo $S^{-\infty}_{1,0}$ by the standard composition theorem, and the products $b_L\#a$ and $a\#b_R$ are both equal to $1$ in this quotient. Thus
\begin{align*}
b_L-b_R=(b_L\#a)\#b_R-b_L\#(a\#b_R)\quad\operatorname{mod} S^{-\infty}_{1,0}.
\end{align*}
Associativity makes the right-hand side equal to $0$ modulo $S^{-\infty}_{1,0}$, so
\begin{align*}
b_L-b_R\in S^{-\infty}_{1,0}.
\end{align*}
Set $b=b_L$ and $B_h=\operatorname{Op}_h(b)$. The left identity has already been proved. For the right identity, write
\begin{align*}
a\#b_L-1=(a\#b_R-1)+a\#(b_L-b_R).
\end{align*}
The first term lies in $S^{-\infty}_{1,0}$, and the second term lies in $S^{-\infty}_{1,0}$ because composition with $a\in S^m_{1,0}$ preserves ordinary smoothing order when the other factor is in $S^{-\infty}_{1,0}$. Quantization gives
\begin{align*}
A_hB_h=I+S_h
\end{align*}
for some $S_h\in\Psi_h^{-\infty}(\mathbb{R}^n)$. Together with
\begin{align*}
B_hA_h=I+R_h,
\end{align*}
this proves the theorem exactly with ordinary smoothing remainders.
[/step]
