proposition: Lemma checksubsum_set1 n i (x : 'rV['F_2]_n) : \delta [set i] x = ~~ (bool_of_F2 x ``_ i).
proof: Proof. by rewrite /checksubsum (big_pred1 i) ?negbK // => n2; rewrite in_set1. 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