Monotonic sequences in posets

[malarbol]

This PR introduces a few definitions and results to work with sequences is preorders, posets or strictly preordered sets.
As an application, it introduces the concept of subsequences of a sequence u: the sequences u ∘ f for some strictly increasing map f : ℕ → ℕ.

[malarbol]

There's still a lot to do but if anyone sees anything they dislike, we can start talking about it.
For example, should I use nondecreasing / increasing instead of increasing / strictly increasing ?

[malarbol]

Is it problematic to merge this PR without #1371? It is helpful to me to portion the review job out a bit (2700 lines is a lot for me)

On the contrary! That's why I kept it separated from #1371. I think it's' self-contained enough to be merged on its own and it will make #1371 2/3 lighter, so easier to review later. I'm actually doing last-minute additions there too but it's ok to merge this now and I'll make the necessary changes in #1371 for a new review.

[malarbol]

I added a few modules on bounded sequences. I still haven't find a good name for sequences tending to infinity so I'd rather leave this for later. Otherwise, I think it's good to go.

[fredrik-bakke]

I added a few modules on bounded sequences. I still haven't find a good name for sequences tending to infinity so I'd rather leave this for later. Otherwise, I think it's good to go.

Were these files suggested in the previous review?
If not, please pull them out to a second PR so this one can be merged.

[malarbol]

Were these files suggested in the previous review? If not, please pull them out to a second PR so this one can be merged.

Not really. At some point I wanted to use them to talk about unbounded sequences / sequences tending to infinity but I didn't went through. They're out now.

[fredrik-bakke]

Thank you!