proposition: Lemma size_filter2 d d' : 0 < size (enum X \\ [:: d; d']).
proof: Proof. rewrite size_filter -has_count; apply/hasP. by exists (another d d'); [rewrite another_in | exact: 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