proposition: Lemma nth_transp u v a b i : i != size u -> i != (size u).+1 -> nth inh (u ++ [:: a; b] ++ v) i = nth inh (u ++ [:: b; a] ++ v) i.
proof: Proof. Proof using. move=> Hi Hi1; rewrite !nth_cat. case: (ltnP i (size u)) => //= Hui. have {Hui} Hi : (size u) < i by rewrite ltn_neqAle eq_sym Hui Hi. have {Hi1 Hi} : (size u).+1 < i by rewrite ltn_neqAle eq_sym Hi1 Hi. rewrite -addn1 addSnnS => /(leq_sub2r (size u)); rewrite addnC addnK. by case: (i - (size u)) => [// | [// | j]] _. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools combclass ordtype permcomp