proposition: Lemma rsymrel_anti IS : IS \subset Delta -> antisymmetric (rsymrel IS).
proof: Proof. rewrite /rsymrel => /subsetP HD i j /=. move=> /andP[/or3P[/eqP -> // | jiIS | /andP[iltj ijNIS]]]. - move=> /or3P[/eqP -> // | ijIS | /andP[jlti jiNIS]]. + exfalso. by have:= ltn_trans (DeltaP (HD _ jiIS)) (DeltaP (HD _ ijIS)); rewrite ltnn. + by rewrite jiIS in jiNIS. - move=> /or3P[/eqP -> // | ijIS | /andP[jlti jiNIS]]. + by rewrite ijIS in ijNIS. + exfalso. by have:= ltn_trans iltj jlti; rewrite ltnn. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism presentation) mathcomp(ssralg poly ssrint) permcomp tools permuted combclass congr