### Abstract

We use the previous formalization of the general simplex algorithm to
formulate an algorithm for solving linear programs. We encode the
linear programs using only linear constraints. Solving these
constraints also solves the original linear program. This algorithm is
proven to be sound by applying the weak duality theorem which is also
part of this formalization.