name: `cvgeMl` -> `cvgeMr`?

[IshiguroYoshihiro]

trafficstars

https://github.com/math-comp/analysis/blob/11915720f13a33adf805e33dbfe17f01076e2460/theories/normedtype.v#L2747 https://github.com/math-comp/analysis/blob/11915720f13a33adf805e33dbfe17f01076e2460/theories/normedtype.v#L3105-L3106

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 https://github.com/math-comp/analysis/pull/1580