proposition: Lemma length_max s : length s <= 'C(n, 2).
proof: Proof. by rewrite /length -card_Delta; apply: subset_leq_card (invset_Delta s). Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism presentation) mathcomp(ssralg poly ssrint) permcomp tools permuted combclass congr