Blame | Last modification | View Log | RSS feed
addeqineq:Add an equation to an inequality
addineq:Add two inequalities
addnum:Add a number to the two sides of an inequality
addterm:Add an expression to the two sides of an inequality
constineq:Introduce a constant inequality
divexp:Divide an inequality by an expression
divnum:Divide an inequality by a number
exsides:Exchange the two sides of an inequality
lincomb:Addition of inequalities with coefficients
mulexp:Multiply an inequality by an expression
mulineq:Multiply two inequalities
mulnum:Multiply an inequality by a number
obvineq:Introduce an obvious inequality
rewrite:Rewrite an inequality
simpdeduc:Simple deduction of inequality
splitineq:Separate cases according to an inequality
sqrpos:Positivity of a square
trans:Transitivity of inequalities