proposition: Lemma perm_of_relP (r : rel 'I_n) : injective (fun i : 'I_n => nth i (sort r (enum 'I_n)) i).
proof: Proof. move=> i j /= /eqP. have /(set_nth_default j i)-> : i < size (sort r (enum 'I_n)). by rewrite size_sort size_enum_ord. rewrite nth_uniq => [/eqP/val_inj -> //|||]. - by rewrite size_sort size_enum_ord. - by rewrite size_sort size_enum_ord. - by rewrite sort_uniq enum_uniq. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism presentation) mathcomp(ssralg poly ssrint) permcomp tools permuted combclass congr