Blame | Last modification | View Log | RSS feed
eq/addnum:Add a number to the two sides of an equation
eq/addterm:Add an expression to the two sides of an equation
eq/divnum:Divisde an equation by a number
eq/exsides:Exchange the two sides of an equation
eq/lincomb:Addition of equations with coefficients
eq/mulnum:Multiply an equation by a number
eq/rewrite:Rewrite an equation
eq/spliteq:Separate the cases according to an (in)equation
exp/rewrite:Rewrite an expression
exp/substit:Substitution in an expression
exp/substitg:Substitution in an expression
ineq/addeqineq:Add an equation to an inequality
ineq/addineq:Add two inequalities
ineq/addnum:Add a number to the two sides of an inequality
ineq/addterm:Add an expression to the two sides of an inequality
ineq/constineq:Introduce a constant inequality
ineq/divexp:Divide an inequality by an expression
ineq/divnum:Divide an inequality by a number
ineq/exsides:Exchange the two sides of an inequality
ineq/lincomb:Addition of inequalities with coefficients
ineq/mulexp:Multiply an inequality by an expression
ineq/mulineq:Multiply two inequalities
ineq/mulnum:Multiply an inequality by a number
ineq/obvineq:Introduce an obvious inequality
ineq/rewrite:Rewrite an inequality
ineq/simpdeduc:Simple deduction of inequality
ineq/splitineq:Separate cases according to an inequality
ineq/sqrpos:Positivity of a square
ineq/trans:Transitivity of inequalities
integrate/basic:Basic integration formula
integrate/basic0:Basic integration formula
integrate/byparts:Integration by parts
integrate/chvar:Direct change of variable
integrate/chvarinv:Reverse change of variable
integrate/const:Integration of a constant
integrate/cut:Cut an integration into two
integrate/rewrite:Rewrite an integral
integrate/sincos:Integration formula of sin/cos/sh/ch
prf/cleanhyp:Erase useless hypotheses
prf/contrapose:Contrapose
prf/splitgoal:Prove a goal separately (when there are several)