proposition: Lemma card_Delta : #|Delta| = 'C(n, 2).
proof: Proof. rewrite /Delta -card_ltn_sorted_tuples. have /card_imset <- : injective (fun p : 'II_n => [tuple p.1; p.2]). by move=> [i1 i2] [j1 j2] [-> ->]. congr #|pred_of_set _|; apply/setP => [[[| s0 [| s1 [|s]]]]] // Hs. rewrite inE /=; apply/imsetP/idP => /= [[[i j]] |]; rewrite andbT. - by rewrite inE /= => Hij [-> ->]. - move=> Hsort; exists (s0, s1); first by rewrite inE. exact: val_inj. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism presentation) mathcomp(ssralg poly ssrint) permcomp tools permuted combclass congr