proposition: Lemma mlead_prod_le T (r : seq T) (P : pred T) F : (mlead (\prod_(p <- r | P p) F p) <= (\sum_(p <- r | P p) mlead (F p))%MM)%O.
proof: Proof. elim/big_rec2: _ => /= [|x m p Px ih]; first by rewrite mlead1. by apply/(le_trans (mleadM_le (F x) p)); apply/lem_add. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype tuple finfun bigop finset binomial) mathcomp(order fingroup perm ssralg zmodp poly ssrint) mathcomp(matrix vector) mathcomp(bigenough) ssrcomplements freeg