proposition: Lemma filter_pred1 h : enum X \\ [:: h] != [::].
proof: Proof. rewrite -has_filter; apply/hasP. exists (another h h); first by rewrite mem_enum. by move: (another_notin h h); apply: contra; rewrite !inE => ->. 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