  Solutions to differential equations, which are used to model physical
systems, are computed numerically by solving a set of discretized equations.
This set of discretized equations is reduced to a large linear system, whose
solution is typically found using an iterative solver. We start with an initial
guess, $x_0$, and iterate the algorithm to obtain a sequence of solution
vectors, $x_k$, which are approximations to the exact solution of the linear
system, $x$. The iterative algorithm is said to converge to $x$, in the field
of reals, if and only if $x_k$ converges to $x$ in the limit of $k \to \infty$.
  In this paper, we formally prove the asymptotic convergence of a particular
class of iterative methods called the stationary iterative methods, in the Coq
theorem prover. We formalize the necessary and sufficient conditions required
for the iterative convergence, and extend this result to two classical
iterative methods: the Gauss--Seidel method and the Jacobi method. For the
Gauss--Seidel method, we also formalize a set of easily testable conditions for
iterative convergence, called the Reich theorem, for a particular matrix
structure, and apply this on a model problem of the one-dimensional heat
equation. We also apply the main theorem of iterative convergence to prove
convergence of the Jacobi method on the model problem.
