use infotheo here

[affeldt-aist]

https://github.com/affeldt-aist/trajectories/blob/a0a147cf08c3f3a5eebef5a559c0487be241bcdf/theories/conv.v#L82

this is already defined in infotheo where unfortunately the type of standard reals is hard-wired
generalization is in progress (see affeldt-aist/infotheo#100) (this is not the case anymore since infotheo 0.9.0)

@yoshihiro503