proposition: Lemma alt_straight_step (m : 'X_{1..n}) (i : nat) : i < n0 -> m (inord i.+1) != 0%N -> 'a_(m + rho) = - 'a_(m # 's_i - U_(inord i) + U_(inord i.+1) + rho).
proof: Proof. rewrite /alternpol => ltin0 mi1. have ltin : i < n by apply: ltnW. rewrite -sumrN [RHS](reindex_inj (mulgI 's_i)); apply eq_bigr => /= s _. rewrite odd_mul_tperm inordi_neq_i1 //= signrN scaleNr opprK. rewrite msymMm; congr (_ *: msym _ _); rewrite msymX; congr ('X_[_]). apply/mnmP => j; rewrite !mnmE permKV eltrV. case: (inord i =P j) => [<-{j} /= | /eqP neqij]. rewrite eltrL eqxx (negbTE (inordi_neq_i1 _)) //= subn0. by rewrite !inordK // -addnA subn1 add1n subnSK. case: (inord i.+1 =P j) => [<-{j neqij} /= | /eqP neqi1j]. rewrite tpermR eqxx eq_sym (negbTE (inordi_neq_i1 _)) // !inordK //=. rewrite addn0; case: (m (inord i.+1)) mi1 => // mi1 _. by rewrite addSnnS [(mi1.+1 - 1)%N]subSS subn0 subnSK // subn1. by rewrite tpermD // (negbTE neqij) (negbTE neqi1j) subn0 addn0. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(ssralg ssrint fingroup perm) mathcomp(mpoly) tools combclass ordtype sorted partition tableau skewpart skewtab antisym Schur_mpoly freeSchur therule std stdtab unitriginv presentSn