proposition: Lemma PCM_V (c : 'rV['F_2]__) : H *m c ^T = 0 -> forall m0, \big[+%R/Zp0]_(n0 < n | n0 \in 'V m0) c ``_ n0 = 0.
proof: Proof. move=> Hsyndrome m0. have : (H *m c^T) m0 ord0 = 0 by rewrite Hsyndrome mxE. rewrite mxE => <-. rewrite [in RHS](bigID (fun j => H m0 j == 0)) /=. rewrite [in RHS](eq_bigr (fun=> 0)); last by move=> ? /eqP ->; rewrite mul0r. rewrite [in RHS]big1 // add0r. apply congr_big => //. move=> x. by rewrite -F2_eq1 VnextE //= sym_tanner_rel // /tanner_rel /=; unlock. move=> n1 n1m0; rewrite (_ : H _ _ = 1) ?mul1r ?mxE //. apply/eqP; by move: n1m0; rewrite VnextE /tanner_rel; unlock. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix) bigop_ext ssralg_ext f2 subgraph_partition