proposition: Lemma betaE p n k : prime p -> beta p n k = logn p (n`!) - logn p (\prod_(0 <= i < k) (n %/ a i)`!).
proof: Proof. move => Hprime; rewrite -(logn_div p); last first. by rewrite -(C_multi n k) dvdn_mulr. by rewrite -(C_multi n k) mulKn //; apply: prodn_gt0=> i; apply: fact_gt0. Qed.
imports: mathcomp(all_ssreflect all_algebra) extra_mathcomp tactics floor arithmetics multinomial