Def submodule.canonically_ordered_add_monoid

refactor(src/algebra/order/monoid): make bot_eq_zero a simp lemma only when the order is linear (#14553)

feat(algebra/{lie/subalgebra,module/submodule/pointwise}): submodules and lie subalgebras form canonically ordered additive monoids under addition (#14529) …