proposition: Lemma another_another p h : h != p -> another 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 another_sym another_bc. by rewrite (another_sym b) another_ab another_ac. by rewrite another_sym another_ac. by rewrite (another_sym c) another_ac another_ab. by rewrite (another_sym c) another_bc another_sym another_ab. 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