proposition: Lemma prods_wordcd_inj c1 c2 : c1 \is a code -> c2 \is a code -> size c1 = n -> size c2 = n -> 's_[wordcd c1] = 's_[wordcd c2] -> c1 = c2.
proof: Proof. Proof using. move=> Hc1 Hc2 Hsz1 Hsz2. have HC1 : is_code_of_size n c1 by rewrite /is_code_of_size Hc1 Hsz1 /=. have HC2 : is_code_of_size n c2 by rewrite /is_code_of_size Hc2 Hsz2 /=. by move/((bij_inj prods_codesz_bij) (CodeSZ HC1) (CodeSZ HC2))/(congr1 val). Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism presentation) mathcomp(ssralg poly ssrint) permcomp tools permuted combclass congr