[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.[/step]

[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: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]