In a non-commutative ring, to test whether a set of polynomials involving $m$ variables, where $m$ is symbolic instead of numeric, is a Gröbner basis of an ideal, the S-polynomial reduction test must be done inductively, which may be very complicated. The defining ideal of the quaternionic polynomial ring in $m$ quaternionic variables is a typical example, where it is not difficult to predict a Gröbner basis based on the results from small values of $m$, but it is extremely difficult to make the verification by finishing all the S-polynomial reductions inductively. In this paper, we present a computer-assisted inductive proof on a Gröbner basis of the defining ideal of quaternionic polynomial ring. We develop two techniques in the course of the proof: left-to-right decomposition, which provides a much weaker test for Gröbner basis, and subdivision and rewriting of interval variables, which preserves the leading term in rewriting monomials as new variables and successive reductions. Both techniques may be extended to more general non-commutative setting involving $m$ variables. With the help of an improved computer-assisted proving program and a modern workstation, the entire Main Theorem can be proven in as fast as 42 minutes.