Metamath Proof Explorer
Table of Contents - 20.34. Mathbox for Stanislas Polu
- inductionexd
- IMO Problems
- IMO 1972 B2
- INT Inequalities Proof Generator
- int-addcomd
- int-addassocd
- int-addsimpd
- int-mulcomd
- int-mulassocd
- int-mulsimpd
- int-leftdistd
- int-rightdistd
- int-sqdefd
- int-mul11d
- int-mul12d
- int-add01d
- int-add02d
- int-sqgeq0d
- int-eqprincd
- int-eqtransd
- int-eqmvtd
- int-eqineqd
- int-ineqmvtd
- int-ineq1stprincd
- int-ineq2ndprincd
- int-ineqtransd
- N-Digit Addition Proof Generator
- unitadd
- AM-GM (for k = 2,3,4)
- gsumws3
- gsumws4
- amgm2d
- amgm3d
- amgm4d