Editorial: refactor remainder AOs

[michaelficarra]

Extracted from #2901. Makes the wording consistent and clearly separates the aliases being declared from the ones being referenced.

[bakkot]

Works for me.

[jmdyck]

There's no need to define _r_ and _q_ 'simultaneously' though. So it'd be simpler to just split each into 2 steps, roughly:

Let _q_ be the integer/BigInt ....
Let _r_ be _n_ - (_d_ x _q_). 

[jmdyck]

(Also, I don't think there's a good reason for the differences in how _q_ is defined.)

[jmdyck]

Since 5.2.5 defines floor(), I think you could say:

Let _quotient_ be ℝ(_n_) / ℝ(_d_).
Let _q_ be the mathematical value whose sign is the sign of _quotient_
   and whose magnitude is floor(abs(_quotient_)).

If you want, you could add a Note-step saying how the sign of _quotient_ relates to the signs of _n_ and _d_.

[michaelficarra]

Thanks @jmdyck. I accepted your suggestion.

[syg]

So I'm fine with this landing, and in particular I think the BigInt reformulation is a strictly clearer wording. That said I prefer this not be precedent-setting for requiring an alias for all intermediates. I want us to be still able to judiciously use where clauses where clear.