proposition: Lemma eltr_comm i j : i.+1 < j < n0 -> 's_i * 's_j = 's_j * 's_i.
proof: Proof. Proof using. move=> /andP[Hij Hj]. have Hi := ltn_trans Hij Hj. apply: tpermC; rewrite /eq_op /=. - by rewrite inord1i // inordi // (ltn_eqF (ltnW Hij)). - by rewrite !inordi // (ltn_eqF Hij). - rewrite inord1i // inordi1 //. by rewrite (ltn_eqF (leq_trans (ltnW Hij) (leqnSn j))). - rewrite inordi // inordi1 //. by rewrite eqSS (ltn_eqF (ltnW Hij)). Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism presentation) mathcomp(ssralg poly ssrint) permcomp tools permuted combclass congr