proposition: Lemma transitive_DeltaI1 IS : (transitive (srel (Delta :\: IS))) <-> (forall i j k : 'I_n, i < j < k -> (i, k) \in IS -> ((i, j) \in IS \/ (j, k) \in IS)).
proof: Proof. split. - rewrite /= => tr i j k /andP[iltj jltk] ik. case: (boolP ((i, j) \in IS)) => [_ | ijN]/=; first by left. right; move: ik; apply/contraLR => jkN. have {}/tr tr : (i, j) \in Delta :\: IS by rewrite !inE ijN /= iltj. have {}/tr : (j, k) \in Delta :\: IS by rewrite !inE jkN /= jltk. by rewrite /= inE => /andP[]. - move=> H j i k; rewrite /= !inE /= ![_ && (_ < _)]andbC. move=> /andP[iltj ijN] /andP[jltk jkN]. rewrite (ltn_trans iltj jltk) /=. have ijk : i < j < k by rewrite iltj jltk. move: ijN; apply contra => /(H i j k ijk) [] //. by rewrite (negbTE jkN). Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism presentation) mathcomp(ssralg poly ssrint) permcomp tools permuted combclass congr