proposition: Lemma alt_straight_add_ribbon0 (p : seq nat) (i : 'I_n) (d : nat) : is_part p -> size p <= n -> add_ribbon p d i == None -> 'a_(mpart p + rho + U_(i) *+ d.+1) = 0%R.
proof: Proof. rewrite /add_ribbon => Hpart Hsz. case: startrem (startremE p d.+1 i) (startrem_leq_pos p d.+1 i) => a [|b]//= . rewrite addn0 => Heq leai _. move: leai; rewrite leq_eqVlt => /orP[/eqP Hai | ltai]. by exfalso; move: Heq => /eqP; rewrite Hai -[X in X == _]addn0 !eqn_add2l. have ltan := ltn_trans ltai (ltn_ord i). set mon := (M in 'a_(M)). suff /alt_alternate -> : mon i = mon (Ordinal ltan) => //. by rewrite -val_eqE /= (gtn_eqF ltai). apply/eqP; rewrite {}/mon !mnmE !mpartE //=. rewrite !mulmnE !mnm1E eqxx -val_eqE mul1n /= (gtn_eqF ltai) mul0n addn0. rewrite addnAC -(eqn_add2r (a + i)) {1}(addnC a i) -!addnA. rewrite subn1 /= ![(n0 - _) + _]addnA !subnK -?[i <= n0]ltnS //. rewrite ![(n0 - _) + _]addnA !subnK -?[i <= n0]ltnS //. by rewrite ![n0 + _]addnC !addnA [_ + _ + a]addnAC Heq. 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