proposition: Lemma enum_fdist_binary_supp : enum (fdist_supp d) = fdist_binary_supp0 :: fdist_binary_supp1 :: [::].
proof: Proof. apply (@eq_from_nth _ fdist_binary_supp0); first by rewrite -cardE Hd. case=> [_ |]; first by rewrite [X in _ = X]/= {2}/fdist_binary_supp0 (enum_val_nth fdist_binary_supp0). case=> [_ |i]; last by rewrite -cardE Hd. by rewrite [X in _ = X]/= {1}/fdist_binary_supp1 (enum_val_nth fdist_binary_supp0). Qed.
imports: mathcomp(all_ssreflect ssralg fingroup perm matrix) mathcomp(all_algebra vector reals normedtype) mathcomp(mathcomp_extra boolp) mathcomp(Rstruct) ssrR logb realType_ext ssr_ext ssralg_ext bigop_ext