fact: Definition rsymrel IS := [rel i j : 'I_n | [|| (i == j), (j, i) \in IS | (i < j) && ((i, j) \notin IS)]].
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism presentation) mathcomp(ssralg poly ssrint) permcomp tools permuted combclass congr