proposition: Lemma approx_mxStar H y : y <=* mxStar H.
proof: Proof. apply/'forall_forallP => /= m0 ord1. apply/forallP => /= n0; rewrite !mxE; by case: ifP => [|] _. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix) ssr_ext ssralg_ext num_occ f2 ssrR hamming tanner linearcode