proposition: Lemma dom_by_uniform (R: realType) A (P : fdist R A) n (An1 : #|A| = n.+1) : P `<< fdist_uniform An1.
proof: Proof. apply/dominatesP => a; rewrite fdist_uniformE => /esym abs; exfalso. by move: abs; rewrite An1; apply/eqP; rewrite lt_eqF // invr_gt0 ltr0n. 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