proposition: Lemma not_trivial_replcode : not_trivial RepLcode.
proof: Proof. rewrite /not_trivial /=. exists (const_mx 1)%R. rewrite Rep.const_mx_in_code /=. by apply/eqP => /matrixP/(_ ord0 ord0); rewrite !mxE. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix mxalgebra vector) hamming num_occ ssralg_ext f2 linearcode decoding channel_code