fact: Definition invset s : {set 'II_n} := [set p : 'II_n | (p.1 < p.2) && (s p.1 > s p.2) ].
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism presentation) mathcomp(ssralg poly ssrint) permcomp tools permuted combclass congr