Abstract: 
We formalize results about linear inqualities, mainly from
Schrijver's book. The main results are the proof of the
fundamental theorem on linear inequalities, Farkas' lemma,
Carathéodory's theorem, the FarkasMinkowskyWeyl theorem, the
decomposition theorem of polyhedra, and Meyer's result that the
integer hull of a polyhedron is a polyhedron itself. Several theorems
include bounds on the appearing numbers, and in particular we provide
an apriori bound on mixedinteger solutions of linear inequalities. 
BibTeX: 
@article{Linear_InequalitiesAFP,
author = {Ralph Bottesch and Alban Reynaud and René Thiemann},
title = {Linear Inequalities},
journal = {Archive of Formal Proofs},
month = jun,
year = 2019,
note = {\url{http://isaafp.org/entries/Linear_Inequalities.html},
Formal proof development},
ISSN = {2150914x},
}
