proposition: Lemma indexed_partition (I T : finType) (J : {pred I}) (B : I -> {set T}) : let P := [set B i | i in J] in {in J &, forall i j : I, j != i -> [disjoint B i & B j]} -> (forall i : I, J i -> B i != set0) -> partition P (cover P) /\ {in J &, injective B}.
proof: Proof. move=> P disjB inhB; have s0NP : set0 \notin P. by apply/negP => /imsetP[x xI /eqP]; apply/negP; rewrite eq_sym inhB. by rewrite /partition eqxx s0NP andbT /=; apply: trivIimset. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop)