- This avoids confusion between
_authsuffix in the algebra name no longer makes sense, so I removed it.
- This makes the names between the logic and the algebra-level liobrary consistent.
- I also renamed
_lbin 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.