update using MathComp 1.17.0 naming convention

[affeldt-aist]

analysis/theories/constructive_ereal.v

Line 3163 in 9c311a9

Lemma lte_pdivl_mull r y x : (0 < r)%R -> (x < r^-1%:E * y) = (r%:E * x < y).