mulrEDr, mulrEDl should be renamed to muleDr, muleDl

[t6s]

analysis/theories/ereal.v

Lines 1478 to 1486 in 39c80bd

	Lemma mulrEDr x y z : x \is a fin_num -> y +? z -> x * (y + z) = x * y + x * z.
	Proof.
	rewrite /mule/=; move: x y z => [x| |] [y| |] [z| |] //= _; try
	(by case: ltgtP => // -[] <-; rewrite ?(mul0r,add0r,adde0))
	|| (by case: ltgtP => //; rewrite adde0).
	by rewrite mulrDr.
	Qed.
	Lemma mulrEDl x y z : x \is a fin_num -> y +? z -> (y + z) * x = y * x + z * x.

The lemmas mulrEDr and mulrEDl does not seem to be following the conventional naming pattern: shouldn't they be muleDr and muleDl?