proposition: Lemma mlead_sum_le {T} (r : seq T) P F : (mlead (\sum_(p <- r | P p) F p) <= \join_(p <- r | P p) mlead (F p))%O.
proof: Proof. elim/big_rec2: _ => /= [|x m p Px le]; first by rewrite mlead0. by apply/(le_trans (mleadD_le _ _))/leU2. 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