proposition: Lemma encode_inj : injective encode.
proof: Proof. rewrite /injective => a b; rewrite /encode 2!ffunE. exact: (@full_rank_inj _ _ _ 'G dimlen rank_GEN). Qed.
imports: mathcomp(all_ssreflect ssralg poly polydiv fingroup perm) mathcomp(finalg zmodp matrix mxalgebra mxpoly vector) ssr_ext ssralg_ext poly_ext f2 hamming decoding channel_code