proposition: Lemma mlead_sum {T} (r : seq T) P F : uniq [seq mlead (F x) | x <- r & P x] -> mlead (\sum_(p <- r | P p) F p) = (\join_(p <- r | P p) mlead (F p))%O.
proof: Proof. elim: r=> [|p r ih]; first by rewrite !big_nil mlead0. rewrite !big_cons /=; case: (P p)=> //= /andP[Fp_ml uq_ml]. pose Q i := P (nth p r i); rewrite !(big_nth p) -!(big_filter _ Q). set itg := [seq _ <- _ | _]; have [/size0nil->|nz_szr] := eqVneq (size itg) 0%N. by rewrite !big_nil joinx0 addr0. move: {ih}(ih uq_ml); rewrite !(big_nth p) -!(big_filter _ Q) -/itg. move=> ih; rewrite mleadD ih //. case: bigjoinP; [exact: le_total | by rewrite /nilp; case: eqP nz_szr |]. move=> /= x; rewrite mem_filter => /andP[Px]. rewrite mem_iota add0n subn0 => /andP[_ lt_x_szr]. apply/contra: Fp_ml=> /eqP-> {Q itg uq_ml nz_szr ih}. elim: r x Px lt_x_szr=> [|y r ih] [|x] //=. by move=> -> /=; rewrite mem_head. rewrite ltnS=> Px lt_x_szr; case: (P y)=> /=. by rewrite 1?mem_behead //=; apply/ih. by apply/ih. 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