proposition: Lemma neq_a x : x != a -> (x == b) || (x == c).
proof: Proof. have : x \in X by []. by rewrite -mem_enum enumE !inE => /orP[->|]. 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