proposition: Lemma another_bc : another b c = a.
proof: Proof. rewrite /another; case: pickP => /= [x|]. have : x \in enum X by rewrite mem_enum. by rewrite enumE !inE => /or3P[] /eqP ->; rewrite ?eqxx //= ?andbF. move/(_ a). by rewrite a_neq_b a_neq_c. 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