Vass: This repository contains following formalizations: logic/LRA.v: Linear real arithmetic and Fourier-Motzkin elimination; logic/Presburger.v: Presburger arithmetic and quantifier elimination; algebra_ext.v: Quantifier elimination principle for linear inequalities; matrix_ext.v: Farkas’ lemma; cone.v: Elementary theory of convex cones.