Name suggestions for mod_add_div' and div_add_mod'

Stream: general

[Julian Külshammer]

In #5884 I have started trying to resolve issue #1534. The basic question is to what the names of division with remainder should be (and how many of them should be there). There are four variations:

• r+bq: This is currently called mod_add_div. (And before this PR existed for nat, pnat, int.)
• bq+r: This is currently called div_add_mod. (And before this PR existed for euclidean_domain and ordinal.)
• qb+r: This currently doesn't exist, but looks to me like the most common version one would find in a text book.
• r+qb : This currently doesn't exist.

In the issue, Scott just called the non-existing div_add_mod and mod_add_div'. In the PR review, @Eric Wieser suggested renaming all of them taking the naming convention literally and adding a mul, so e.g. the first one would become mod_add_mul_div. What is your opinion? Should the missing two be added? Any opinion or suggestion on the name?