This is an unofficial reimagining of the Archive of Formal Proofs
Linear Inequalitiesby Ralph Bottesch, Alban Reynaud and René Thiemann