proposition: Lemma reduced_wcord c : rev c \is a code -> size c <= n.+1 -> wcord c \is reduced.
proof: Proof. Proof using. move=> Hc Hsz; rewrite wcordE //. by apply reduced_sprod_code; last by rewrite size_rev. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism presentation) mathcomp(ssralg poly ssrint) permcomp tools permuted combclass congr