m stands for
_mono added, the
_auth suffix in the algebra name no longer makes
sense, so I removed it.
_lb in the algebra-level library so as to
make it consistent with the logic-level library.
Furthermore make the order of lemmas consistent and make the versions for the fractions consistent.