proposition: Lemma supp_fdist1 : fdist_supp fdist1 = [set a] :> {set A}.
proof: Proof. apply/setP => a0; rewrite !inE. have [->|a0a] := eqVneq a0 a; first by rewrite fdist1E eqxx oner_eq0. by apply/negbTE; rewrite negbK fdist1E (negbTE a0a). 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