introduce the category of Bounded posets

[fchapoton]

as an useful thing to have

also declare that finite lattices are bounded

📝 Checklist

• The title is concise and informative.
• The description explains in detail what this PR is about.
• I have created tests covering the changes.
• I have updated the documentation and checked the documentation preview.

[fchapoton]

Would it be better to put "Bounded" lower in the list of axiom names ?

EDIT: It seems not.

[tscrim]

LGTM modulo one detail and one potential improvement.

[fchapoton]

Here is a way to make the "bounded finite" disappear.