feat(order/*): introduces complemented lattices (#5747)
Defines `is_complemented` on bounded lattices
Proves facts about complemented modular lattices
Provides two instances of `is_complemented` on submodule lattices
Co-authored-by: Johan Commelin <johan@commelin.net>
Co-authored-by: Aaron Anderson <65780815+awainverse@users.noreply.github.com>
