https://github.com/math-comp/analysis/blob/36680bc768401672853271c9981a0c48555c4ab5/theories/itv.v#L431 "The multiplication only works for realDomainType (and not for numDomainType), for relatively bad reasons."