proposition: Lemma fdist_card_neq0 d : (0 < #| A |)%nat.
proof: Proof. apply/negPn/negP => abs. have /eqP := oner_neq0 R; apply. rewrite -(FDist.f1 d) (eq_bigl xpred0) ?big_pred0_eq // => a. apply/negP => aA. by move/card_gt0P : abs; apply; exists a. 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