proposition: Lemma head_filter def h p x : x \in [:: h; p] -> head def (enum X \\ [:: h; p]) != x.
proof: Proof. move=> xhp. have : x \notin enum X \\ [:: h; p] by rewrite mem_filter xhp. apply: contra => /eqP {1}<-. rewrite -nth0 mem_nth // lt0n size_eq0 -has_filter; apply/hasP. by exists (another h p); [rewrite mem_enum | rewrite another_notin]. 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