A lemma (entry) may depend on lemmas (entries) below its position, but never on lemmas
above its position. This means the list is a topological order of the dependency graph.
An entry 'all subs proved' means that all used lemmas are (transitively) proved.
| Name: | Status: | Subs proved? | Used: |
|---|
| absls-05 | proved | all subs proved
| sub-add-09,
sub-sub,
mone-01,
sub-add-01,
num-subadd,
Minus-def,
abs-08,
abs-05,
mone-06,
numls-02,
elim-sub,
le-def,
sub-pred,
succ-02,
sub-ls,
abs-16,
abs-09,
|
| abs-10 | proved | all subs proved
| abs-zero,
lsone,
sub-ls,
|
| absp-01 | proved | all subs proved
| abs-ls-02,
|
| abs-le-succ | proved | all subs proved
| succ-02,
numlelsdel,
forward-le-02,
numls-03,
sub-sub-03,
sub-zero,
sub-le,
Minus-def,
abs-08,
num-subadd,
sub-sub,
abs-05,
le-def,
Abs-pos,
|
| abs-ls-02 | proved | all subs proved
| sub-ls-01,
abssub-02,
sub-eq,
abs-06,
Abs-pos,
elim-sub,
le-def,
|
| abs-zero | proved | all subs proved
| abs-06,
le-def,
|
| abs-05 | proved | all subs proved
| le-def,
numle-03,
abseq,
sub-eq,
sub-sub,
Abs-neg,
|
| absls-04 | proved | all subs proved
| sub-eq-01,
sub-eq,
abs-06,
sub-pred,
le-def,
sub-ls-01,
abs-16,
abs-09,
|
| absa | proved | all subs proved
| Abs-pos,
abseq,
sub-add,
sub-add-01,
sub-zero,
zero-gels-01,
forward-le-02,
sub-eq,
Minus-def,
abs-08,
le-def,
|
| abs-04 | proved | all subs proved
| numadd,
absle,
abs-12,
|
| zero-not | proved | all subs proved
| sub-ls-01,
abs-06,
Abs-pos,
abs-16,
zero-gels-01,
forward-le-02,
forward-le-05,
sub-ls,
Minus-def,
abs-08,
le-def,
|
| abs-12 | proved | all subs proved
| zero-gs,
le-def,
abs-18,
absle,
|
| abseq | proved | all subs proved
| Abs-pos,
sub-sub-03,
sub-zero,
Minus-def,
abs-08,
le-def,
abs-16,
|
| abs-09 | proved | all subs proved
| lels-03,
lsone,
le-def,
sub-le-01,
abs-18,
abs-16,
|
| abs-06 | proved | all subs proved
| forward-le-05,
abs-16,
zero-gels-01,
sub-ls-01,
Minus-def,
abs-08,
|
| absp | proved | all subs proved
| zero-gels-01,
abs-ls-03,
abs-16,
le-def,
|
| abs-01 | proved | all subs proved
| Abs-pos,
sub-sub-03,
sub-zero,
sub-eq,
Minus-def,
abs-08,
abssub-02,
|
| abs-21 | proved | all subs proved
| sub-sub-03,
absneg-01,
Abs-pos,
sub-zero,
zero-gels-01,
forward-le-02,
abs-08,
sub-eq,
Minus-def,
|
| abs-wfind | proved | all subs proved
| absls,
le-def,
abs-03,
nat-wfind,
|
| absone-02 | proved | all subs proved
| abs-succ,
le-def,
|
| abs-ls-01 | proved | all subs proved
| zero-gels-01,
abs-ls-03,
abs-16,
le-def,
|
| abs-one-01 | proved | all subs proved
| lsone,
abs-16,
lels-03,
mone-06,
numls-03,
sub-ls-01,
Minus-def,
abs-08,
le-def,
|
| absneg | proved | all subs proved
| sub-sub-03,
sub-zero,
sub-eq,
Minus-def,
absneg-01,
|
| absneg-02 | proved | all subs proved
| sub-sub-03,
sub-zero,
sub-eq,
Minus-def,
absneg-01,
|
| abs-neg | proved | all subs proved
| Abs-pos,
abs-16,
forward-le-02,
sub-eq,
abs-08,
elim-sub,
Minus-def,
|
| absone | proved | all subs proved
| abs-succ,
le-def,
|
| abssub-04 | proved | all subs proved
| sub-add,
sub-add-01,
abssub,
|
| abssub-03 | proved | all subs proved
| sub-add,
sub-add-01,
abssub,
|
| numabspos | proved | all subs proved
| absle,
|
| abs-sub-02 | proved | all subs proved
| succ-01,
sub-le-01,
sub-add-05,
sub-add-01,
sub-le,
abssub-01,
abssub-02,
|
| abssub-01 | proved | all subs proved
| succ-01,
sub-le-01,
abs-18,
|
| abssub | proved | all subs proved
| lenls,
le-def,
sub-le-01,
abs-18,
|
| abs-succ | proved | all subs proved
| numls-03,
le-def,
succ-02,
Abs-pos,
lels-03,
mone-06,
sub-ls,
num-subadd,
sub-sub,
sub-add-09,
mone-01,
sub-add-01,
numadd-01,
sub-eq,
Minus-def,
abs-08,
zero-gels-01,
forward-le-02,
|
| abs-03 | proved | all subs proved
| absls,
le-def,
|
| absneg-01 | proved | all subs proved
| sub-sub-03,
sub-zero,
Minus-def,
abs-08,
le-def,
abs-18,
sub-eq,
|
| absle | proved | all subs proved
| zero-gels-04,
abs-18,
|
| abssub-02 | proved | all subs proved
| le-def,
sub-le-01,
abs-18,
|
| abs-16 | proved | all subs proved
| le-def,
abs-18,
|
| abs-17 | proved | all subs proved
| le-def,
numle-02,
abs-18,
|
| abs-19 | proved | all subs proved
| absls-01,
le-def,
|
| abs | proved | all subs proved
| zero-gels,
le-def,
abs-18,
|
| abs-11 | proved | all subs proved
| absls,
numls-03,
forward-le-02,
|
| abs-sub | proved | all subs proved
| absls-01,
elim-sub,
|
| absone-01 | proved | all subs proved
| numls-02,
forward-le-05,
Abs-pos,
sub-ls,
mone-01,
sub-add-09,
sub-sub,
minus-add,
sub-add-01,
numadd-01,
sub-eq,
Minus-def,
abs-08,
zero-gels-01,
forward-le-02,
|
| absle-01 | proved | all subs proved
| absls-02,
le-def,
|
| negone | proved | all subs proved
| sub-add-09,
sub-sub,
mone-01,
sub-add-01,
sub-eq,
num-subadd,
sub-pred,
Minus-def,
|
| abssub-05 | proved | all subs proved
| zero-gels-01,
abs-18,
elim-sub,
le-def,
succ-02,
|
| minus-01 | proved | all subs proved
| sub-add-09,
sub-sub,
mone-01,
sub-add-01,
sub-eq,
num-subadd,
Minus-def,
|
| absls-02 | proved | all subs proved
| forward-le-05,
Abs-pos,
sub-ls-01,
sub-zero,
zero-gels-01,
forward-le-02,
sub-ls,
Minus-def,
abs-08,
le-def,
|
| nat-wfind | proved | all subs proved
| forward-le-05,
lsone,
sub-ls,
sub-pred,
succ-01,
sub-le-01,
succ-02,
mone-06,
numls-03,
zero-gels-01,
anti,
le-def,
|
| absls-01 | proved | all subs proved
| Abs-pos,
sub-ls,
Minus-def,
abs-08,
|
| abs-18 | proved | all subs proved
| Abs-pos,
le-def,
sub-eq,
Minus-def,
abs-08,
|
| absls | proved | all subs proved
| Abs-pos,
sub-ls,
Minus-def,
abs-08,
zero-gels-01,
forward-le-02,
|
| abs-ls-03 | proved | all subs proved
| zero-gels-01,
sub-ls-01,
Minus-def,
abs-08,
elim-sub,
|
| mone-01 | proved | all subs proved
| numsub,
sub-add-01,
sub-eq,
minus-add,
|
| absls-06 | proved | all subs proved
| sub-ls-01,
Minus-def,
abs-08,
Abs-pos,
|
| neg-11 | proved | all subs proved
| sub-sub-03,
sub-zero,
Minus-def,
sub-add-09,
sub-eq,
sub-sub,
|
| absls-03 | proved | all subs proved
| sub-ls-01,
Minus-def,
abs-08,
Abs-pos,
|
| ler | proved | all subs proved
| numsub,
sub-add-01,
sub-le,
sub-pred,
le-def,
numle-01,
|
| numlsf | proved | all subs proved
| succ-01,
|
| abs-add | proved | all subs proved
| sub-sub-03,
sub-zero,
Minus-def,
abs-08,
|
| neg-02 | proved | all subs proved
| sub-zero-01,
minus-sub,
Minus-def,
|
| k-sub-rec1 | proved | all subs proved
| numadd,
sub-add-02,
sub-add-01,
sub-eq,
sub-sub-04,
sub-pred,
|
| k-sub-rec2 | proved | all subs proved
| sub-add,
sub-add-01,
sub-add-06,
sub-eq,
sub-sub,
sub-pred,
|
| minus | proved | all subs proved
| numadd,
minus-neg,
minus-sub,
num-subadd,
sub-sub,
Minus-def,
|
| abs-07 | proved | all subs proved
| Abs-pos,
sub-eq,
Minus-def,
abs-08,
|
| abs-14 | proved | all subs proved
| forward-le-05,
forward-le-02,
sub-ls,
Minus-def,
abs-08,
|
| abs-15 | proved | all subs proved
| forward-le-02,
forward-le-05,
sub-ls,
Minus-def,
abs-08,
le-def,
|
| bet | proved | all subs proved
| num-between,
|
| abs-ls-04 | proved | all subs proved
| sub-ls,
Minus-def,
abs-08,
zero-gels-01,
forward-le-02,
le-def,
|
| numabsneg | proved | all subs proved
| sub-sub-03,
sub-zero,
sub-eq,
Minus-def,
abs-08,
|
| sub-add-08 | proved | all subs proved
| numsub,
sub-add-01,
sub-add-05,
sub-eq,
sub-sub,
|
| sub-add-07 | proved | all subs proved
| numadd,
sub-add-02,
sub-add-01,
sub-eq,
|
| subsub | proved | all subs proved
| sub-sub-03,
sub-zero,
Minus-def,
sub-add-09,
sub-eq,
sub-sub,
|
| sub-add-04 | proved | all subs proved
| numsub,
sub-add-01,
sub-eq,
sub-add-05,
sub-sub,
|
| sub-add-03 | proved | all subs proved
| numadd,
sub-add-02,
sub-sub-04,
|
| lepr | proved | all subs proved
| succ-01,
sub-le-01,
sub-pred,
|
| ls-rew-succ | proved | all subs proved
| succ-01,
|
| sub-sub-02 | proved | all subs proved
| numadd,
sub-add-02,
sub-add-01,
sub-eq,
sub-sub-04,
|
| ple-01 | proved | all subs proved
| sub-ls,
sub-add-01,
sub-pred,
succ-02,
forward-le-05,
le-def,
|
| neg-eq | proved | all subs proved
| sub-zero-01,
minus-sub,
Minus-def,
|
| le-rec | proved | all subs proved
| notle-pos,
sub-le-01,
succ-01,
le-def,
|
| minus-02 | proved | all subs proved
| sub-add,
sub-add-01,
sub-eq,
sub-zero,
Minus-def,
minus-sub,
|
| abs-ls | proved | all subs proved
| sub-ls-01,
sub-zero,
Minus-def,
abs-08,
zero-gels-01,
numls-03,
forward-le-02,
sub-ls,
|
| numlsf-02 | proved | all subs proved
| succ-01,
|
| nat-structind | proved | all subs proved
| forward-le-05,
lsone,
sub-ls,
sub-pred,
succ-01,
sub-le-01,
lels-03,
succ-02,
mone-06,
numls-03,
anti,
le-def,
|
| sub-add-05 | proved | all subs proved
| numsub,
sub-add-01,
sub-eq,
sub-add-06,
|
| num-between | proved | all subs proved
| lels-03,
succ-02,
le-def,
numle-01,
|
| minus-add | proved | all subs proved
| sub-zero-01,
sub-sub-04,
Minus-def,
|
| minus-neg | proved | all subs proved
| sub-add,
sub-add-01,
sub-eq,
sub-zero,
Minus-def,
|
| sub-add-02 | proved | all subs proved
| numadd,
sub-add,
|
| minus-sub | proved | all subs proved
| sub-add,
sub-add-01,
sub-eq,
sub-sub-04,
Minus-def,
|
| succ-01 | proved | all subs proved
| lels-03,
succ-02,
le-def,
|
| abs-08 | proved | all subs proved
| sub-sub-03,
sub-zero,
sub-eq,
Minus-def,
Abs-neg,
|
| num-subadd | proved | all subs proved
| sub-add,
sub-add-01,
sub-add-06,
sub-eq,
sub-sub,
|
| sub-add-09 | proved | all subs proved
| sub-sub-03,
sub-zero,
sub-eq,
Minus-def,
|
| sub-pred | proved | all subs proved
| numsub,
sub-add-01,
|
| sub-eq-01 | proved | all subs proved
| sub-sub-03,
|
| neg-12 | proved | all subs proved
| sub-eq,
sub-zero,
Minus-def,
|
| neg-06 | proved | all subs proved
| sub-sub-03,
sub-zero,
sub-eq,
Minus-def,
|
| neg-03 | proved | all subs proved
| sub-sub-03,
sub-zero,
Minus-def,
|
| neg-09 | proved | all subs proved
| sub-ls-01,
sub-zero,
Minus-def,
|
| neg-08 | proved | all subs proved
| sub-ls,
sub-zero,
Minus-def,
|
| les | proved | all subs proved
| lels-03,
succ-02,
le-def,
numle-01,
|
| neg-01 | proved | all subs proved
| sub-ls-01,
sub-zero,
sub-ls,
Minus-def,
|
| negadd | proved | all subs proved
| sub-ls-01,
sub-zero,
sub-ls,
Minus-def,
|
| num-eq-shift | proved | all subs proved
| sub-eq,
sub-zero,
Minus-def,
sub-add,
sub-add-01,
|
| sub-same | proved | all subs proved
| sub-add,
sub-sub-04,
|
| numlef | proved | all subs proved
| le-def,
succ-02,
sub-ls,
|
| minus-rew | proved | all subs proved
| sub-add,
sub-add-01,
sub-eq,
sub-zero,
Minus-def,
|
| mone-04 | proved | all subs proved
| le-def,
mone-06,
numle-02,
|
| mone-07 | proved | all subs proved
| forward-le-02,
lels-03,
mone-06,
le-def,
numadd-01,
|
| mone-03 | proved | all subs proved
| numadd-01,
sub-eq,
Minus-def,
|
| neg-15 | proved | all subs proved
| sub-add,
sub-add-01,
sub-eq,
sub-zero,
Minus-def,
|
| sub-sub-01 | proved | all subs proved
| sub-add,
sub-add-01,
sub-add-06,
sub-eq,
sub-sub,
|
| sub-minus | proved | all subs proved
| sub-add,
sub-add-01,
sub-eq,
sub-sub-04,
sub-zero,
sub-sub,
Minus-def,
|
| subneg | proved | all subs proved
| sub-zero-01,
sub-sub-04,
Minus-def,
|
| numlef-01 | proved | all subs proved
| le-def,
succ-02,
sub-ls,
|
| le-rew-succ | proved | all subs proved
| le-def,
succ-02,
|
| abs-sub-01 | proved | all subs proved
| Abs-pos,
numls-03,
sub-add,
numls-02,
numadd-01,
elim-sub,
le-def,
|
| neg-add | proved | all subs proved
| sub-sub-03,
sub-zero,
Minus-def,
|
| numadd-01 | proved | all subs proved
| sub-eq,
sub-add,
|
| numle-03 | proved | all subs proved
| le-def,
sub-le-01,
|
| numle-02 | proved | all subs proved
| le-def,
sub-le,
|
| sub-zero-01 | proved | all subs proved
| sub-eq,
|
| numadd | proved | all subs proved
| sub-eq,
sub-add-01,
|
| sub-sub-04 | proved | all subs proved
| sub-add,
sub-add-01,
sub-eq,
|
| numle-01 | proved | all subs proved
| le-def,
sub-le-01,
sub-add-01,
|
| numsub | proved | all subs proved
| sub-add,
sub-add-01,
sub-eq,
|
| sub-sub-03 | proved | all subs proved
| sub-eq,
|
| sub-zero | proved | all subs proved
| sub-add,
sub-add-01,
sub-eq,
|
| succ-02 | proved | all subs proved
| numls-01,
le-def,
|
| sub-sub | proved | all subs proved
| sub-add,
sub-add-01,
sub-eq,
sub-add-06,
|
| add-rew | proved | all subs proved
| sub-eq,
sub-add,
|
| negeq | proved | all subs proved
| sub-eq,
Minus-def,
|
| neg-10 | proved | all subs proved
| sub-eq,
Minus-def,
|
| negle-13 | proved | all subs proved
| le-def,
sub-le,
Minus-def,
|
| negle-07 | proved | all subs proved
| le-def,
sub-le-01,
Minus-def,
|
| zeroone | proved | all subs proved
| bet-01,
le-def,
|
| rew-eqzero | proved | all subs proved
| sub-eq,
Minus-def,
|
| sub-less | proved | all subs proved
| forward-le-05,
le-def,
sub-le-01,
|
| mone-neg | proved | all subs proved
| not-mone,
|
| sub-shift | proved | all subs proved
| sub-add,
sub-add-01,
sub-eq,
|
| lsls-add-notgr | proved | all subs proved
| numls-03,
forward-le-05,
|
| neg-14 | proved | all subs proved
| sub-eq,
Minus-def,
|
| le-sub-same | proved | all subs proved
| le-def,
sub-add,
sub-add-01,
sub-le,
|
| one-03 | proved | all subs proved
| sub-eq,
lsone,
sub-ls-01,
sub-add,
sub-add-01,
forward-le-05,
le-def,
|
| add-shift | proved | all subs proved
| sub-eq,
sub-add,
|
| rew-eqzero-01 | proved | all subs proved
| sub-eq,
Minus-def,
|
| sub-shift-second | proved | all subs proved
| sub-add,
sub-add-01,
sub-eq,
|
| le-add-01 | proved | all subs proved
| zero-gels-01,
le-def,
sub-le,
ge-def,
|
| numls-01 | proved | all subs proved
| sub-ls-01,
sub-add-01,
|
| not-mone | proved | all subs proved
| zero-gs,
le-def,
|
| numls-03 | proved | all subs proved
| sub-ls-01,
|
| bet-01 | proved | all subs proved
| anti,
lsone,
|
| sub-le-01 | proved | all subs proved
| sub-ls,
le-def,
|
| sub-le | proved | all subs proved
| sub-ls-01,
le-def,
|
| numls-02 | proved | all subs proved
| sub-ls,
|
| sub-eq | proved | all subs proved
| sub-add,
sub-add-01,
|
| neg-13 | proved | all subs proved
| sub-ls,
Minus-def,
|
| neg-05 | proved | all subs proved
| sub-ls,
Minus-def,
|
| neg-07 | proved | all subs proved
| zero-gels-01,
sub-ls-01,
Minus-def,
|
| not-mtwo | proved | all subs proved
| zero-gs,
le-def,
|
| ex-le-add | proved | all subs proved
| sub-ls,
sub-add,
sub-add-01,
le-def,
|
| minus-gr | proved | all subs proved
| sub-ls,
gr-def,
Minus-def,
|
| ple-02 | proved | all subs proved
| notle-pos,
|
| sub-ls-02 | proved | all subs proved
| sub-ls,
sub-add-01,
|
| neg | proved | all subs proved
| zero-gels-01,
sub-ls-01,
Minus-def,
|
| le-add-07 | proved | all subs proved
| zero-gels-01,
forward-le-05,
le-def,
ge-def,
le-add-02,
lels,
|
| le-add-06 | proved | all subs proved
| zero-gels-01,
le-def,
ge-def,
le-add-02,
lels,
|
| le-add-05 | proved | all subs proved
| zero-gels-01,
forward-le-05,
le-def,
ge-def,
le-add-02,
lels,
|
| le-add-04 | proved | all subs proved
| zero-gels-01,
le-def,
ge-def,
le-add-02,
|
| le-add-08 | proved | all subs proved
| zero-gels-01,
forward-le-05,
lels,
ge-def,
le-def,
le-add-02,
|
| lels | proved | all subs proved
| le-def,
lenls,
|
| le-add-02 | proved | all subs proved
| zero-gels-01,
le-def,
ge-def,
|
| notle-pos | proved | all subs proved
| zero-gels-01,
le-def,
|
| zero-gs | proved | all subs proved
| zero-gels-01,
forward-le-02,
le-def,
|
| anti | proved | all subs proved
| lenls,
le-def,
|
| sub-add-06 | proved | all subs proved
| sub-add,
elim-sub,
|
| sub-ls | proved | all subs proved
| elim-sub,
|
| sub-add-01 | proved | all subs proved
| sub-add,
elim-sub,
|
| sub-ls-01 | proved | all subs proved
| elim-sub,
|
| zero-ge | proved | all subs proved
| zero-gels-01,
forward-le-02,
le-def,
|
| lels-add-notgr | proved | all subs proved
| lsle-add-notgr,
|
| lels-add-notge | proved | all subs proved
| lsle-add-notge,
|
| lels-add-noteq | proved | all subs proved
| lsle-add-noteq,
|
| le-add-03 | proved | all subs proved
| zero-gels-01,
le-def,
ge-def,
|
| lsle-add-noteq | proved | all subs proved
| forward-le-05,
le-def,
|
| lsle-add-notge | proved | all subs proved
| forward-le-05,
le-def,
|
| lenls | proved | all subs proved
| lels-03,
|
| lsle-add-notgr | proved | all subs proved
| forward-le-05,
le-def,
|
| zero-gels-01 | proved | all subs proved
| forward-le-02,
le-def,
|
| elim-sub | proved | all subs proved
| Sub-def,
sub-add,
|
| int-add-pos-01 | proved | all subs proved
| forward-le-05,
le-def,
|
| sub-same-01 | proved | all subs proved
| sub-add,
|
| discard-add2-lels-left | proved | all subs proved
| forward-le-05,
le-def,
|
| leone | proved | all subs proved
| lels-03,
lsone,
le-def,
|
| forward-le-01 | proved | all subs proved
| forward-le-02,
le-def,
|
| forward-le-03 | proved | all subs proved
| forward-le-02,
le-def,
|
| forward-le-04 | proved | all subs proved
| forward-le-05,
le-def,
|
| mone-08 | proved | all subs proved
| lels-03,
mone-06,
le-def,
|
| mone-05 | proved | all subs proved
| lels-03,
mone-06,
le-def,
|
| mone-02 | proved | all subs proved
| numlelsdel,
|
| int-add-pos | proved | all subs proved
| forward-le-05,
le-def,
|
| lsls-add-noteq | proved | all subs proved
| forward-le-05,
|
| lstwo | proved | all subs proved
| lstwo-01,
|
| lep-02 | proved | all subs proved
| le-def,
le-add,
|
| le-three | proved | all subs proved
| le-def,
forward-le-05,
numlsf-01,
|
| forward-le | proved | all subs proved
| forward-le-05,
le-def,
|
| numlsf-01 | proved | all subs proved
| le-def,
|
| le-add | proved | all subs proved
| le-def,
|
| lstwo-01 | proved | all subs proved
| le-def,
|
| zero-gels-04 | proved | all subs proved
| le-def,
|
| numlelsdel | proved | all subs proved
| le-def,
|
| zero-gels | proved | all subs proved
| le-def,
|
| lsone | proved | all subs proved
| le-def,
|
| lels-03 | proved | all subs proved
| le-def,
|
| forward-le-05 | proved | all subs proved
| le-def,
|
| forward-le-02 | proved | all subs proved
| le-def,
|
| mone-06 | proved | all subs proved
| le-def,
|
| sub-add | proved | all subs proved
| Sub-def,
|
| estimate-add2-ls-left | proved | all subs proved
| le-def,
|
| estimate-add2-lsle-left | proved | all subs proved
| le-def,
|
| lep | proved | all subs proved
| le-def,
|
| estimate-add1-ls-right | proved | all subs proved
| le-def,
|
| forward-lele | proved | all subs proved
| le-def,
|
| numleledel-01 | proved | all subs proved
| le-def,
|
| forward-lels | proved | all subs proved
| le-def,
|
| estimate-add1-lsle-left | proved | all subs proved
| le-def,
|
| numleledel | proved | all subs proved
| le-def,
|
| numlslsdel | proved | all subs proved
| le-def,
|
| transrew | proved | all subs proved
| le-def,
|
| transrew-01 | proved | all subs proved
| le-def,
|
| pls-01 | proved | all subs proved
| le-def,
|
| estimate-add2-le-right | proved | all subs proved
| le-def,
|
| ge | proved | all subs proved
| ge-def,
le-def,
|
| lsls-add-notge | proved | all subs proved
| le-def,
|
| estimate-add2-ls-right | proved | all subs proved
| le-def,
|
| zero-gels-03 | proved | all subs proved
| le-def,
|
| estimate-add1-le-right | proved | all subs proved
| le-def,
|
| int-add-same-pos | proved | all subs proved
| gr-def,
|
| zero-gels-02 | proved | all subs proved
| le-def,
|
| lele-add-notgr | proved | all subs proved
| le-def,
|
| estimate-add1-ls-left | proved | all subs proved
| le-def,
|
| zero-ge-01 | proved | all subs proved
| le-def,
|
| ple-04 | proved | all subs proved
| le-def,
|
| estimate-add2-le-left | proved | all subs proved
| le-def,
|
| ple-03 | proved | all subs proved
| le-def,
|
| estimate-add2-lsle-right | proved | all subs proved
| le-def,
|
| numlelsdel-01 | proved | all subs proved
| le-def,
|
| ttwo | proved | all subs proved
| le-def,
|
| lep-01 | proved | all subs proved
| le-def,
|
| zero-eq | proved | all subs proved
| le-def,
|
| estimate-add1-lsle-right | proved | all subs proved
| le-def,
|
| estimate-add1-le-left | proved | all subs proved
| le-def,
|
| lels-02 | proved | all subs proved
| le-def,
|
| numlsledel-01 | proved | all subs proved
| le-def,
|
| numlsledel | proved | all subs proved
| le-def,
|
| numlslsdel-02 | proved | all subs proved
| le-def,
|
| numlslsdel-03 | proved | all subs proved
| le-def,
|
| numlslsdel-01 | proved | all subs proved
| le-def,
|
| add-pos-ge | proved | all subs proved
| ge-def,
|
| int-simp-11 | proved | all subs proved
| le-def,
|
| forward-lsle | proved | all subs proved
| le-def,
|
| ple | proved | all subs proved
| le-def,
|
| pls | proved | all subs proved
| le-def,
|
| Sub-def | axiom | | |
| ge-def | axiom | | |
| gr-def | axiom | | |
| Abs-neg | axiom | | |
| Abs-pos | axiom | | |
| Minus-def | axiom | | |
| le-def | axiom | | |