proposition: Lemma mutual_indeE' : #|I| != O -> mutual_inde <-> kwide_inde #|I| d E.
proof: Proof. move=> I0. rewrite /mutual_inde; split => [H J JI|]. have [->{J JI}|J0] := eqVneq J set0. by rewrite !big_set0 Pr_setT. by rewrite (H #|J|.-1) ?prednK // card_gt0. by move=> H k J Jk; rewrite H // max_card. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum matrix) mathcomp(Rstruct reals) Reals Lra ssrR Reals_ext realType_ext logb ssr_ext ssralg_ext bigop_ext fdist