Added automatic proofs related to elimination rules of inequalities.