proposition: Lemma repair_odd (r : nat) (Hr : odd r.+1) x : @repair r x != None.
proof: Proof. rewrite /repair /majority_vote ffunE. case: ifPn => //; by rewrite Hr /= andbF. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix mxalgebra vector) hamming num_occ ssralg_ext f2 linearcode decoding channel_code