proposition: Lemma approx_BEC_input_mxStar : approx_BEC_input H y (mxStar H).
proof: Proof. case: BEC_y => c cy; exists c => //; exact: approx_mxStar. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix) ssr_ext ssralg_ext num_occ f2 ssrR hamming tanner linearcode