proposition: Lemma filter1_another h p : h != p -> enum X \\ [:: p] = [:: h; another h p] \/ enum X \\ [:: p] = [:: another h p; h].
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 // => _; rewrite ?another_ab ?another_ac ?another_bc //. by rewrite /= !inE a_neq_b eqxx /= eq_sym b_neq_c; left. by rewrite /= !inE a_neq_c b_neq_c eqxx; left. by rewrite /= !inE eqxx /= eq_sym a_neq_b eq_sym a_neq_c another_sym another_ab; left. rewrite /= !inE a_neq_c b_neq_c eqxx /=; by right. rewrite /= !inE eqxx /= eq_sym a_neq_b eq_sym a_neq_c another_sym another_ac; by right. rewrite /= !inE a_neq_b eqxx /= eq_sym b_neq_c another_sym another_bc; by right. 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