proposition: Lemma comb_dprojs d A (g : A -> {set 'I_n}) t : (forall n0, t ``_ n0 = d ``_ n0 \/ exists a, n0 \in g a) -> comb d (dprojs d g t) g = t.
proof: Proof. move=> K. apply/rowP => n1. rewrite /comb; unlock => /=; rewrite mxE. case: pickP => [/= a Ha | ]; first by rewrite dprojs_in. move=> /= Hpred0. case: {K}(K n1) => [ //| [a Ha]]. exfalso. move: (Hpred0 a); by rewrite Ha. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg zmodp matrix) Reals mathcomp(Rstruct) ssr_ext ssralg_ext ssrR Reals_ext f2 summary subgraph_partition tanner tanner_partition fdist channel checksum