proposition: Lemma logn_prod (I : Type) (r : seq I) F p : (forall i : I, 0 < F i) -> logn p (\prod_(i <- r) F i) = \sum_(i <- r) logn p (F i).
proof: Proof. move => H; elim: r => [|a l Hl]; first by rewrite !big_nil logn1. rewrite !big_cons lognM ?Hl //; exact: prodn_gt0. Qed.
imports: mathcomp(all_ssreflect all_algebra)