proposition: Lemma sumn_cocode s : sumn (cocode s) = length s.
proof: Proof. have /= := cocode2P s => [] [Hcode {2}->]. by rewrite -length_permcd // size_cocode. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism presentation) mathcomp(ssralg poly ssrint) permcomp tools permuted combclass congr