Details | Last modification | View Log | RSS feed
| Rev | Author | Line No. | Line |
|---|---|---|---|
| 20 | reyssat | 1 | eq:addnum addterm divnum exsides lincomb mulnum rewrite spliteq |
| 2 | eq/addnum:Add a number to the two sides of an equation |
||
| 3 | eq/addterm:Add an expression to the two sides of an equation |
||
| 4 | eq/divnum:Divide an equation by a non-zero number |
||
| 5 | eq/exsides:Exchange the two sides of an equation |
||
| 6 | eq/lincomb:Addition of equations with coefficients |
||
| 7 | eq/mulnum:Multiply an equation by a non-zero number |
||
| 8 | eq/rewrite:Rewrite an equation |
||
| 9 | eq/spliteq:Separate the cases according to an (in)equation |
||
| 10 | exp:rewrite substit substitg |
||
| 11 | exp/rewrite:Algebraic rewriting of an expression |
||
| 12 | exp/substit:Substitution in an algebraic expression global or partial |
||
| 13 | exp/substitg:Substitution in a global algebraic expression global or partial |
||
| 14 | ineq:addeqineq addineq addnum addterm constineq divexp divnum exsides lincomb mulexp mulineq mulnum obvineq rewrite simpdeduc splitineq sqrpos trans |
||
| 15 | ineq/addeqineq:Add an equation to an inequality |
||
| 16 | ineq/addineq:Add two inequalities |
||
| 17 | ineq/addnum:Add a number to the two sides of an inequality |
||
| 18 | ineq/addterm:Add an expression to the two sides of an inequality |
||
| 19 | ineq/constineq:Introduce a constant inequality |
||
| 20 | ineq/divexp:Divide an inequality by an expression of constant sign |
||
| 21 | ineq/divnum:Divide an inequality by a non-zero number |
||
| 22 | ineq/exsides:Exchange the two sides of an inequality |
||
| 23 | ineq/lincomb:Addition of inequalities with coefficients |
||
| 24 | ineq/mulexp:Multiply an inequality by an expression of constant sign |
||
| 25 | ineq/mulineq:Multiply two positive inequalities |
||
| 26 | ineq/mulnum:Multiply an inequality by a non-zero number |
||
| 27 | ineq/obvineq:Introduce an obvious inequality after simple arithmetics |
||
| 28 | ineq/rewrite:Rewrite an inequality |
||
| 29 | ineq/simpdeduc:Simple deduction of inequality |
||
| 30 | ineq/splitineq:Separate cases according to an inequality |
||
| 31 | ineq/sqrpos:The square of a real number is positive or zero |
||
| 32 | ineq/trans:Apply the transitivity of inequalities |
||
| 33 | integrate:basic basic0 byparts chvar chvarinv const cut rewrite sincos |
||
| 34 | integrate/basic:Basic integration formula |
||
| 35 | integrate/basic0:Minimal basic integration formula |
||
| 36 | integrate/byparts:Integration by parts |
||
| 37 | integrate/chvar:Direct change of variable |
||
| 38 | integrate/chvarinv:Reverse change of variable |
||
| 39 | integrate/const:Integration of a constant |
||
| 40 | integrate/cut:Cut an integration into two |
||
| 41 | integrate/rewrite:Rewrite an integral |
||
| 42 | integrate/sincos:Integration formula of sin/cos/sh/ch |
||
| 43 | prf:cleanhyp contrapose splitgoal |
||
| 44 | prf/cleanhyp:Erase useless hypotheses |
||
| 45 | prf/contrapose:Contrapose |
||
| 46 | prf/splitgoal:Prove a goal separately (when there are several) |