Conv set

[t6s]

This PR renews the implementation of necset_convType in terms of conv_set rather than defining another similar but different convex combination operation.

As a byproduct, this PR also contains all of boolean_prob branch and a module for open intervals ( Module OProb ). The latter simplifies some computations that appear when handling convexity.

[affeldt-aist]

Note that:

• lemmas prob_probb, probb_prob, oprob_oprobb, oprobb_oprob are subsumed by lemmas leR2P and ltR2P now in master
• lemma oprob_prob already existed as lemma closed in the file binary_symmetric_channel (used also in ldpc.v) and is now in Reals_ext.v
• the boolean prob PR has been merged in master where above lemmas are present, so you might want to rebase

[t6s]

Note that:

• lemmas prob_probb, probb_prob, oprob_oprobb, oprobb_oprob are subsumed by lemmas leR2P and ltR2P now in master
• lemma oprob_prob already existed as lemma closed in the file binary_symmetric_channel (used also in ldpc.v) and is now in Reals_ext.v
• the boolean prob PR has been merged in master where above lemmas are present, so you might want to rebase

Thank you for summarizing the current state. I will soon update the branch to accommodate these changes.