proposition: Lemma checksubsum_D1 i x : i \in A -> \delta A x = (F2_of_bool (\delta (A :\ i) x) != x ``_ i).
proof: Proof. move=> iA; rewrite /checksubsum (bigD1 i) //=. rewrite (_ : \sum_(i0 in A | i0 != i) x ``_ i0 = \sum_(n0 in A :\ i) x ``_ n0); last first. apply eq_bigl => j; by rewrite in_setD1 andbC. rewrite addr_eq0 eq_sym oppr_char2 //. case/F2P : (x ``_ i) => //=. apply/idP/idP; [by move=> ->|]. by case/boolP : (\sum_(n0 in _) _ == _). apply/idP/idP; [by move/eqP => -> |]. rewrite -F2_eq0; by case: F2P. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix vector) Reals ssralg_ext ssrR Reals_ext f2 fdist channel tanner linearcode pproba