proposition: Lemma checksubsum_add n0 n1 x y (d : 'rV_n) (l : seq 'I_n) : n1 != n0 -> n0 \notin l -> n1 \notin l -> (x + y != \delta [set x in l] (d `[ n1 := x + y]))%R = (y != \delta [set x in n0 :: l] ((d `[ n0 := x]) `[ n1 := y])).
proof: Proof. move=> n1_n0 n0_l n1_l. congr (negb _). rewrite GRing.addrC eq_sym -GRing.subr_eq eq_sym /=. congr (_ == _). rewrite (row_setC _ _ _ n1_n0) (GRing.oppr_char2 _ x) //. rewrite {2}/checksubsum [in X in _ = X](bigD1 n0) /=; last by rewrite !inE eqxx. rewrite !mxE eqxx. rewrite GRing.addrC /checksubsum F2_of_bool_addr. congr (F2_of_bool ((_ + _)%R == _)). apply congr_big => // i. rewrite !inE. case/boolP : (i == n0) => [ /eqP -> | ] /=. by apply/negbTE. by rewrite andbT. rewrite !inE !mxE. case/boolP : (i == n0) => [/eqP -> | ]. by rewrite (negbTE n0_l). case/boolP : (i == n1) => [/eqP -> | //]. by rewrite (negbTE n1_l). Qed.
imports: Wf_nat Init.Wf Recdef Reals mathcomp(all_ssreflect perm zmodp matrix ssralg) mathcomp(Rstruct) ssrR Reals_ext ssr_ext ssralg_ext bigop_ext f2 fdist channel pproba linearcode subgraph_partition tanner tanner_partition summary ldpc checksum ldpc_algo