proposition: Lemma filter_another h p : h != p -> enum X \\ [:: h; p] = [:: another h p].
proof: Proof. have : h \in enum X by rewrite mem_enum. rewrite enumE !inE => /or3P[] /eqP ->; (have : p \in enum X by rewrite mem_enum); rewrite enumE !inE => /or3P[] /eqP ->; rewrite ?eqxx //= !inE ?eqxx ?orbT /=; rewrite ?(negbTE a_neq_b) ?(negbTE a_neq_c) ?(negbTE b_neq_c) ?orbF /=; rewrite ?(eq_sym c) ?(negbTE b_neq_c) /= ?(negbTE a_neq_c) /=; rewrite ?(eq_sym b) ?(negbTE a_neq_b) /= => _. by rewrite another_ab. by rewrite another_ac. by rewrite another_sym another_ab. by rewrite another_bc. by rewrite another_sym another_ac. by rewrite another_sym another_bc. 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