affeldt-aist / infotheo

A Coq formalization of information theory and linear error-correcting codes
GNU Lesser General Public License v2.1
64 stars 15 forks source link

Lemma names Prob.ge0 and prob_le0 are not uniform #42

Closed t6s closed 3 years ago

t6s commented 3 years ago

Prob.ge0 should be placed outside Module Prob and named prob_ge0.