potential generalization from `realDomainType` to `numDomainType`

[affeldt-aist]

analysis/theories/ereal.v

Line 2037 in d46de60

Lemma lee_wpmul2l x : 0 <= x -> {homo *%E x : y z / y <= z}.

analysis/theories/ereal.v

Line 2266 in d46de60

Lemma lte_pmul x1 y1 x2 y2 :

analysis/theories/ereal.v

Line 2279 in d46de60

Lemma lee_pmul x1 y1 x2 y2 : 0 <= x1 -> 0 <= x2 -> x1 <= y1 -> x2 <= y2 ->

(also lee_pmul2l and lee_pmul2r)

[CohenCyril]

Sure, for this kind of change, anything that typechecks!