proposition: Lemma alt_straight_add_ribbon (p : seq nat) (i : 'I_n) (d : nat) : is_part p -> size p <= n -> forall res h, add_ribbon p d i = Some (res, h) -> 'a_(mpart p + rho + U_(i) *+ d.+1) = (-1) ^+ h.-1 *: 'a_(mpart res + rho).
proof: Proof. rewrite /alternpol => Hpart ltsn res h Hrib. have := size_add_ribbon Hrib; move: Hrib; rewrite /add_ribbon. case startremeq : startrem (startrem_leq_pos p d.+1 i) => [start rem]// lesti. case: ltnP => // lt0rem [<- <-] /= Hsz. have starto := leq_ltn_trans lesti (ltn_ord i). have : start = val (Ordinal starto) by []. move: (Ordinal starto) => st Hstart; subst start. rewrite (reindex_inj (mulgI 's_[iota st (i - st)]^-1)%g) /= scaler_sumr. apply: eq_bigr => s _; rewrite scalerA; congr (_ *: _). rewrite odd_permM odd_permV -odd_size_permE; first last. apply/allP => j; rewrite mem_iota /= subnKC // => /andP[_]. by move/leq_ltn_trans/(_ (ltn_ord i)). by rewrite size_iota signr_addb signr_odd. rewrite msymMm msymX invgK; congr (msym s 'X_[_]). apply mnmP => j; rewrite !mnmE !mpartE //; first last. by rewrite Hsz geq_max ltsn ltn_ord. rewrite !mulmnE !mnm1E -val_eqE /=. have := startrem_leq p d.+1 i; rewrite startremeq => /(_ lt0rem) /= lesmin. case: (j =P st) => [/= eqjst | /eqP]. subst j; apply/eqP. rewrite (nth_add_ribbon_start _ lesmin) cycleij_j // eqxx mul1n. rewrite addnAC -(eqn_add2r (st + i)) {1}(addnC st i) -!addnA. rewrite subn1 /= ![(n0 - _) + _]addnA !subnK -?[i <= n0]ltnS //. rewrite ![(n0 - _) + _]addnA !subnK -?[i <= n0]ltnS //. rewrite ![n0 + _]addnC !addnA [_ + _ + i]addnAC [_ + _ + st]addnAC. by have:= startremE p d.+1 i; rewrite startremeq => ->. rewrite neq_ltn => /orP[ltjst | ltstj]. rewrite cycleij_lt // nth_add_ribbon_lt_start //. by rewrite (gtn_eqF (leq_trans ltjst lesti)) mul0n addn0. case: (ltnP i j) => [/= ltij | leji]. rewrite nth_add_ribbon_stop_lt // cycleij_gt //. by rewrite (ltn_eqF ltij) mul0n addn0. rewrite -(ltn_predK ltstj) nth_add_ribbon_in //; first last. by rewrite (ltn_predK ltstj) ltstj leji. rewrite cycleij_in ?ltstj ?leji // inordK; first last. by rewrite (ltn_predK ltstj) /= ltnW. case: j ltstj leji => [[|j]//= Hj] _ /gtn_eqF ->. by rewrite mul0n addn0 addSnnS subnSK // subn1. 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