$AB=I$ implies $BA=I$ in a $M_n(R)$ when $R$ is a semiring?

Question

Let $R$ be a unitary commutative semi-ring and let $M_n(R)$ be the semi-ring of $n \times n$ matrices with coefficients in $R$. Let's call $I$ the identity matrix in $M_n(R)$ (it exists because $R$ is unitary).

Is it true that for any $A$ and $B$ in $M_n(R)$ such that $AB=I$ we have $BA=I$?

Answer 1

This is proven in Inversion of Matrices over a Commutative Semiring by Reutenauer and Straubing. The proofs aren't especially short though (as you request in the comments). The first two paragraphs give good context for their paper though:

It is a well-known consequence of the elementary theory of vector spaces that if $A$ and $B$ are $n$-by-$n$ matrices over a field (or even a skew field) such that $AB = 1$, then $BA = 1$. This result remains true for matrices over a commutative ring, however, it is not, in general, true for matrices over noncommutative rings.

In this paper we show that if $A$ and $B$ are $n$-by-$n$ matrices over a commutative semiring, then the equation $AB = 1$ implies $BA = 1$. We give two proofs: one algebraic in nature, the other more combinatorial. Both proofs use a generalization of the familiar product law for determinants over a commutative semiring.

It's worth mentioning that "semi-ring" for them requires having a multiplicative identity, so they do prove the result you desire.