proposition: Lemma length_maxpermE s : length s = 'C(n, 2) -> s = (@maxperm n).
proof: Proof. move=> Hlen; apply/invset_inj/eqP. rewrite eqEcard -!/(length _) Hlen length_maxperm leqnn andbT. by rewrite invset_maxperm invset_Delta. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism presentation) mathcomp(ssralg poly ssrint) permcomp tools permuted combclass congr