We present a formally verified quantifier elimination procedure for the first order theory over linear mixed real-integer
arithmetics in higher-order logic based on a work by Weispfenning. To this end we provide two verified quantifier elimination
procedures: for Presburger arithmitics and for linear real arithmetics.