proposition: Lemma rsymrel_total (IS : {set 'II_n}) : IS \subset Delta -> total (rsymrel IS).
proof: Proof. rewrite /rsymrel => /subsetP HD /= i j /=. case: eqP => //= /eqP Hneq. rewrite eq_sym (negbTE Hneq) /=; apply/orP. case: (boolP ((j, i) \in IS)) => /=[_|ijNIS]; first by left. case: (boolP ((i, j) \in IS)) => /=[_|jiNIS]; first by right. by rewrite !andbT; apply/orP; rewrite -neq_ltn. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism presentation) mathcomp(ssralg poly ssrint) permcomp tools permuted combclass congr