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
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(this is not the case anymore since infotheo 0.9.0)generalization is in progress (see affeldt-aist/infotheo#100)
@yoshihiro503