Changed Order World's abs_le to an if-and-only-if (this was in the text but not the proof), which meant I had to amend Dan's Cauchy --> Bounded slightly (this used the previous abs_le).
Added "shift rule" for sequences, which I used for Series converges --> sequence tends to 0.
Storing this in Series for now (along with my Convergent --> Bounded) but it should maybe move into limits at a later date.
Changed Order World's abs_le to an if-and-only-if (this was in the text but not the proof), which meant I had to amend Dan's Cauchy --> Bounded slightly (this used the previous abs_le).
Added "shift rule" for sequences, which I used for Series converges --> sequence tends to 0. Storing this in Series for now (along with my Convergent --> Bounded) but it should maybe move into limits at a later date.