proposition: Lemma rsymrel_trans IS : is_invset IS -> transitive (rsymrel IS).
proof: Proof. case; rewrite /rsymrel/= => /subsetP HD HIS HDIS j i k /=. move/orP=> [/eqP ->{i}| Hij]; first by []. move/orP=> [/eqP <-{k}| Hjk]; first by rewrite Hij orbT. apply/orP; right; move: Hij Hjk. move=> /orP[jiIS | /andP[iltj ijNIS]] /orP[kjIS | /andP[jltk jkNIS]]; apply/orP. - by left; apply: (HIS j). - case: (ltngtP i k) => [iltk | klti | /val_inj ik]. + right => /=. by move: jkNIS; apply contra => /(HIS _ _ _ jiIS); apply. + left; move: jiIS; apply contraLR => kiNIS. have jlti := ltn_trans jltk klti. have:= HDIS k j i; rewrite /= !inE /= klti jltk jlti !andbT. exact. + by exfalso; subst k; rewrite jiIS in jkNIS. - case: (ltngtP i k) => [iltk | klti | /val_inj ik]. + right => /=. by move: ijNIS; apply contra => /HIS; apply. + left; move: kjIS; apply contraLR => kiNIS. have kltj := ltn_trans klti iltj. have:= HDIS i k j; rewrite /= !inE /= iltj klti kltj !andbT. exact. + by exfalso; subst k; rewrite kjIS in ijNIS. - right. have iltk := ltn_trans iltj jltk. have:= HDIS j i k; rewrite /= !inE /= jltk iltk iltj !andbT. exact. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism presentation) mathcomp(ssralg poly ssrint) permcomp tools permuted combclass congr