proposition: Lemma lengthV s : length s^-1 = length s.
proof: Proof. Proof using. rewrite /length invset_permV card_imset //. by move=> /= [i j] [k l] /= [/perm_inj-> /perm_inj->]. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism presentation) mathcomp(ssralg poly ssrint) permcomp tools permuted combclass congr