Whilst the definition of addition of Cauchy or Dedekind real numbers is "obvious", multiplication is rather more tricky. Unfortunately, most accounts, including [RD], leave it as an "exercise for the reader", without even giving a hint about what the problem is, so the questioner is right to ask about this. The difficulty is intrinsic to multiplication: the only difference in the intuitionistic setting is that we must do the job properly, instead of bodging it by treating positive, zero and negative numbers separately.
The point is that, if you want to achieve precision $\epsilon$ in the product of two numbers, one of which is bounded by $B$, then the other must be given within $\epsilon/B$.
[MD] is not quoted verbatim in the Question, but it is close enough, whilst the accounts in [AH] and [AT] are essentially the same.
[TD] gives a more general account of uniform continuity, taking explicit account of the modulus of convergence of Cauchy sequences (the function that says how far down the sequence you have to go to get a desired accuracy). This is needed elsewhere in constructive analysis.
[BB] has by far the clearest treatment that I have seen of the arithmetic of Cauchy reals, building the modulus into the definition. (I admire this book for its "can do" attitude, not dwelling on the counterexamples.) It gives the explicit (but snappy) proof of correctness for multiplication.
[BT] defines multiplication for Dedekind reals and proves correctness. It shows how Dedekind reals are the limiting case of intervals and also considers "back-to-front" (Kaucher) intervals, which are related to existential quantification just as ordinary intervals are related to universal quantification.
[JC] defines multiplication in a completely novel fashion for Conway (surreal) numbers. This is adapted to multiplication of real numbers in a topos in [PJ].
Since [MD,AH,AT] do not give the explicit answer to the Question, here it is.
As above, $\langle r_n\rangle$ is a Cauchy sequence if $\forall k.\exists n.\forall m.|r_{n+m}-r_n|\lt 2^{-k}$.
We write $\alpha(k)$ for such an $n$ for each given $k$; this is the modulus of convergence.
In particular, with $k=0$, for any Cauchy sequence $\langle r_n\rangle$ there are integers $N=\alpha(0)$ and $K=\log_2(r_N)$ such that $\forall m.-2^{K}\lt r_N-1\lt r_{N+m}\lt r_N+1\lt 2^{K}$.
Let $M$, $L$ and $\beta$ be the corresponding integers and modulus for the Cauchy sequence $\langle s_n\rangle$.
Now, given $h$, let $k\geq h+L+1$, $l\geq h+K+1$, $n\geq\alpha(k)$ and $n\geq\beta(l)$. Then, for all $m$,
$$\begin{eqnarray}
|r_{n+m} s_{n+m} - r_n s_n|
&\leq& |r_{n+m}| |s_{n+m} - s_n| + |r_{n+m} - r_n| |s_n| \\
&\lt& 2^K 2^{-l} + 2^{-k} 2^L \leq 2^{-h}.
\end{eqnarray}$$
Hence $\langle r_n s_n\rangle$ is a Cauchy sequence with modulus
$\gamma(h)=\max(\alpha(h+L+1),\beta(h+K+1))$.
We can avoid considering equivalence of sequences explicitly, by observing that two Cauchy sequences are equivalent iff they are both subsequences of the same Cauchy sequence. Rationals are represented by constant Cauchy sequences and the new operation for them agrees with multiplication of rationals.
This argument amounts to saying that the new operation is continuous with respect to the Euclidean topology. Also, the rationals are dense amongst Cauchy reals. Hence the new operation is the unique continuous extension and it follows that it obeys the usual algebraic laws for multiplication.
[BT] Andrej Bauer and Paul Taylor,
The Dedekind Reals in Abstract Stone Duality,
in Mathematical Structures in Computer Science, 19 (2009) 757-838.
[BB] Errett Bishop and Douglas Bridges, Foundations of Constructive Analysis,
Grundlehren der mathematischen Wissenschaften, Springer-Verlag, 1985.
[JC] John Horton Conway, On Numbers and Games,
Number 6 in London Mathematical Society Monographs. Academic Press, 1976.
Revised edition, 2001, published by A K Peters, Ltd.
[RD] Richard Dedekind, Stetigkeit und irrationale Zahlen, Braunschweig, 1872.
Reprinted in [DW], pages 315–334; English translation, Continuity and Irrational Numbers, in [DE].
[DE] Richard Dedekind, Essays on the theory of numbers, Open Court, 1901;
English translations by Wooster Woodruff Beman; republished by Dover, 1963.
[DW] Richard Dedekind. Gesammelte mathematische Werke, volume 3. Vieweg, Braunschweig, 1932; edited by Robert Fricke, Emmy Noether and Oystein Ore; republished by Chelsea, New York, 1969.
[MD] Michael Dummett, Elements of Intuitionism, Oxford University Press, 2000.
[AH] Arend Heyting, Intuitionism, an Introduction, Studies in Logic and the Foundations of Mathematics, North-Holland, 1956. Third edition, 1971.
[PJ] Peter Johnstone, Topos Theory, London Mathematical Society Monographs 10, Academic Press, 1977.
[AT] Anne Troelstra, Principles of Intuitionism, Lectures presented
at the Summer Conference on Intuitionism and Proof Theory (1968) at
SUNY at Buffalo, NY, Lecture Notes in Mathematics 95, Springer-Verlag, 1969.
[TD] Anne Sjerp Troelstra and Dirk van Dalen, Constructivism in Mathematics, an Introduction,
Number 121 and 123 in Studies in Logic and the Foundations of Mathematics, North-Holland, 1988.
If you know of other explicit accounts of multiplication for Cauchy or Dedekind reals then please give the references in comments below.
