Takafumi Saikawa

~How about renaming `closed` to `lt2W`?~ NB(rei): has been taken care of by PR #52

~Oops this comment was not meant for this issue.~

One concern is that I could not use generic lemmas not so much I originally expected. I am afraid that the usefulness of the ring structure needs to be more...

Oops, `inv` is indeed wrong. I have renamed it `E_opp_RV`. (I would rather keep `neg` for boolean negation.)

I have noticed that this change imports the axiom of choice in proba.v, which I expect cause some controversy. I am now changing my mind to define the ring structure...

@hoheinzollern I can help modifying the proof script into a more mathcomp-ish style. Do you prefer such a change?

I am afraid that, after the merger of monae-hb branch, even the core part now suffers from a heavy dependency starting from Hierarchy Builder.

> In this case, the strategy would be to have a new subdirectory in infotheo for these two libraries > and release infotheo as two opam packages (like it is...

> Keep infotheo for the main package and ssrstd for ssrZ+ssrR (because it provides ssr-like naming for standard library's datatypes)? ssrstd sounds too generic or strong, doesn't it? What about...

I suspect the reason this definition is not documented might be that it is not a good definition. The name suggests that it is pinpointing a (finite) subcover of some...