proposition: Lemma fdist_uniform_neq0 (C : finType) (domain_non_empty : { m : nat | #| C | = m.+1 }) : forall x, @fdist_uniform R _ _ (projT2 domain_non_empty) x != 0.
proof: Proof. move=> c; rewrite fdist_uniformE invr_eq0 pnatr_eq0. by case domain_non_empty => x' ->. 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