proposition: Lemma eltr_exchange i (a b : 'I_n) : i < n0 -> a < b -> 's_i a < 's_i b = (i != a) || (i.+1 != b).
proof: Proof. Proof using. move=> Hi; case: tpermP => [-> | -> | /eqP Ha1 /eqP Hai1]; case: tpermP => [-> | -> | /eqP Hb1 /eqP Hbi1]; rewrite ?(inordi Hi) ?(inordi1 Hi) /= ?ltnn ?trivSimpl //=. - by move=> /ltnW; rewrite leqNgt => /negbTE ->. - by rewrite (ltn_neqAle i.+1 b) => ->; rewrite andbT. - by rewrite ltnS leqnn. - by move/ltnW => ->. - by rewrite ltnS (ltn_neqAle a i) eq_sym => /andP[-> ->]. - by rewrite ltnS ltn_neqAle => -> /=; rewrite eq_sym andbT orbF. - move=> ->; apply esym; apply/orP; left. move: Ha1; apply contra => /eqP Hia. by apply/eqP/val_inj; rewrite /= -Hia inordi. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism presentation) mathcomp(ssralg poly ssrint) permcomp tools permuted combclass congr