name: `cvgeMl` -> `cvgeMr`?

[IshiguroYoshihiro]

analysis/theories/normedtype.v

Line 2747 in 1191572

Lemma cvgMl f a b : f @ F --> a -> (f x * b) @[x --> F] --> a * b.

analysis/theories/normedtype.v

Lines 3105 to 3106 in 1191572

	Lemma cvgeMl f x y : y \is a fin_num ->
	f @ F --> x -> (fun n => y * f n) @ F --> y * x.

I found a confusion of abbreviation l and r.
I think that cvgeMl should be cvgMr, but I am not sure.

NB(2025/04/21): the renaming of cvgMr is still pending.

[affeldt-aist]

Isn't it rather cvgMl that should be cvgMr because the constant is on the right?

But then should the current cvgrM:

Lemma cvgMr g a b : g @ F --> b -> (a * g x) @[x --> F] --> a * b.

be cvgMl or cvgrM? (I tend towards cvgMl)

@CohenCyril @t6

[affeldt-aist]

We'd better do that after PR #1544 is merged

[affeldt-aist]

NB: cvgeMl and cvgeMr have been renamed by this PR #1580