proposition: Lemma another_notin h p : another h p \notin [:: h; p].
proof: Proof. rewrite /another; case: pickP => [x /andP[xh xp]|] /=. by rewrite !inE negb_or xh xp. 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 /= ?orbT /= ?negb_or. move/(_ b); by rewrite eq_sym a_neq_b. move/(_ c); by rewrite eq_sym a_neq_c eq_sym b_neq_c. move/(_ b); by rewrite eq_sym a_neq_b b_neq_c. move/(_ c); by rewrite eq_sym b_neq_c eq_sym a_neq_c. move/(_ a); by rewrite a_neq_b. move/(_ a); by rewrite a_neq_b a_neq_c. move/(_ b); by rewrite b_neq_c eq_sym a_neq_b. move/(_ a); by rewrite a_neq_c a_neq_b. move/(_ a); by rewrite 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