proposition: Lemma fdist_uniform_supp_neq0 z : ((`U HC) z != 0 :> R) = (z \in C).
proof: Proof. case/boolP : (z \in C) => [/fdist_uniform_supp_in ->| /fdist_uniform_supp_notin ->]. by rewrite invr_neq0// pnatr_eq0 -lt0n. by rewrite eqxx. 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