.. _tac_linarith:

linarith
========

Summary
-------

The ``linarith`` tactic solves certain kind of linear equalities and inequalities. Unlike the ``ring`` tactic, ``linarith`` uses hypotheses in the tactic state.

You can feed extra proofs into ``linarith`` by adding them as a list like this: ``linarith [h1, h2]``. We will see examples of this below.

Examples
--------

To be written. Basically, if you have a bunch of hypotheses like ``h1 : a < b``, ``h2 : b <= c``, ``h3 : c = d`` and a goal of ``a < d`` then ``linarith`` will solve it; it knows a ton of results about how to put inequalities together. As another example if you have hypotheses ``h1 : a < b`` and ``h2 : c < d`` then it will prove a goal ``c + a < b + d``.