proposition: Lemma neq_b x : x != b -> (x == a) || (x == c).
proof: Proof. have : x \in X by []. rewrite -mem_enum enumE !inE => /orP[-> //|/orP[] /eqP ->]; by rewrite ?eqxx // orbT. Qed.
imports: Reals Lra mathcomp(all_ssreflect ssralg ssrnum) mathcomp(mathcomp_extra reals Rstruct) infotheo(ssrR realType_ext Reals_ext proba) monae_lib hierarchy monad_lib fail_lib proba_lib